Theorem imbi2i 185

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

Hypothesis

Ref	Expression
bi.a	|- (ph <-> ps)

Assertion

Ref	Expression
imbi2i	|- ((ch -> ph) <-> (ch -> ps))

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		bi.a	. . . 4 |- (ph <-> ps)
2	1	biimp 151	. . 3 |- (ph -> ps)
3	2	imim2i 17	. 2 |- ((ch -> ph) -> (ch -> ps))
4	1	biimpr 152	. . 3 |- (ps -> ph)
5	4	imim2i 17	. 2 |- ((ch -> ps) -> (ch -> ph))
6	3, 5	impbi 157	1 |- ((ch -> ph) <-> (ch -> ps))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  imbi12i 188  iman 237  orbi2i 255  or12 258  pm4.14 352  pm4.15 353  pm4.78 354  pm4.79 355  anass 441  ibibr 593  bibi2i 610  pm5.32 646  pm5.6 690  nan 691  nicodraw 954  19.35 1077  19.36 1080  sban 1239  2sb6 1338  2sb6rf 1341  eu1 1394  moabs 1417  moanim 1429  2eu6 1457  r2al 1679  r19.21t 1718  r19.35 1762  ralcom2 1779  reu2 1933  reu8 1939  ssconb 2174  reldisj 2318  inssdif0 2338  ssundif 2349  pwpw0 2474  pwsnALT 2506  unissb 2533  dfiin2 2593  ssiun 2597  ssiin 2604  axrep1 2700  dffr2 2926  dfepfr 2939  dffr3 3438  asymref2 3447  fun11 3569  f1fv 3881  inf2 4624  axinf2 4640  aceq1 4746  aceq0 4747  axac 4762  ac6n 4774  kmlem14 4795  aceqkm 4798  zfcndrep 4985  zfcndac 4990  primet 6204  raluz2 6451  cau3ir 6922  clm1 7084  climshft 7111  climres 7112  caucvg 7170  islp2 7751  sncld 7791  lmbr2 7933  iscau2 7941  metcnp4 7974  bcthlem7 8009  nmobndseqi 8443  axgroth4 8782  grothprim 8785  cvnbtwn3t 10218  elat2 10270  anidmdbi 10437

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain