Theorem imbi2d 464

Description: Deduction adding an antecedent to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
imbi2d	|- (ph -> ((th -> ps) <-> (th -> ch)))

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	a1d 14	. 2 |- (ph -> (th -> (ps <-> ch)))
3	2	pm5.74d 444	1 |- (ph -> ((th -> ps) <-> (th -> ch)))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  imbi1d 465  orbi2d 466  bibi2d 470  imbi12d 474  dedlem0a 567  con3th 573  sbcom 916  sbcom2 992  ax15 1006  mo 1020  ralcom2 1314  2gencl 1366  3gencl 1367  vtocl2gf 1385  vtocl2ga 1388  vtocl3ga 1389  mo2icl 1434  sbc5g 1450  sbc6g 1451  sbcel1 1466  sbcel2 1467  axrep 1473  axrep2 1474  bm1.3ii 1481  r19.36zv 1772  dedth2h 1787  dedth3h 1788  dedth4h 1789  elint 1971  elinti 1974  trel 2048  trss 2050  pocl 2132  solin 2145  supeq1 2155  supub 2160  suplub 2161  freq1 2174  dfom2 2374  elom 2375  elomg 2376  findsg 2398  finds2 2399  tfindsg 2402  tfinds2 2405  tfinds3 2406  vtoclr 2449  2optocl 2470  3optocl 2471  resieq 2581  funimaexg 2715  funopfvg 2854  fnfvbr 2855  fvelima 2859  fvelrn 2883  fnressn 2897  fressnfv 2898  f1fveq 2918  tfrlem1 2949  tfr3 2964  ndmoprcl 3058  caoprcan 3069  caoprord 3070  oaordi 3148  nnacl 3172  nnmcl 3173  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmcom 3183  nnmordi 3188  2ecoptocl 3240  3ecoptocl 3241  th3qlem2 3251  inf3lem2 3465  inf3lem5 3468  tz9.1 3490  r1pw 3529  cplem2 3546  karden 3551  aceq4 3557  aceq5lem5 3562  aceq6a 3564  aceq6b 3565  kmlem2 3581  kmlem12 3591  axrepnd 3740  axpowndlem3 3745  zfcndrep 3760  elnp 3886  prlem934a 3931  prlem934 3933  suppr 3957  suppsr 4016  supsrlem6 4024  supre 4054  divmult 4220  divclt 4223  divcan1t 4228  divcan2t 4229  divrect 4238  divdistrt 4246  divcan3t 4251  redivclt 4276  divgt0 4390  ltdivt 4404  ltmuldivt 4406  ltdiv23t 4419  nn1suc 4435  nnaddclt 4436  nnmulclt 4437  nnleltp1t 4448  uzind 4603  uzwo 4605  nnwoOLD 4608  nnwof 4609  indstr 4611  zmax 4618  om2uzlt 4654  seqrn 4673  expcllem 4682  expaddt 4698  replimt 4798  clim 4877  clim2 4881  climunii 4883  hcauchy 5103  hlim 5108  hlim2 5112  hlimcaui 5141  hlimunii 5143  occllem6 5185  projlem7 5199  projlem20 5212  projlem28 5220  projlem29 5221  pjthlem14 5238  pjthut 5243  elspansn2t 5472  pjcjt2 5580  pjss2co 5634  pjssmt 5635  pjopytht 5662  stelt 5671  stcltr1 5707  mdbr 5726  elat2 5739  atcvat2t 5773

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org