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 439  ibibr 590  bibi2i 607  pm5.32 643  pm5.6 687  nan 688  nicodraw 951  19.35 1074  19.36 1077  sban 1236  2sb6 1335  2sb6rf 1338  eu1 1391  moabs 1414  moanim 1426  2eu6 1453  r2al 1674  r19.21t 1713  r19.35 1757  ralcom2 1774  reu2 1927  reu8 1933  ssconb 2167  reldisj 2310  inssdif0 2330  ssundif 2341  pwpw0 2466  unissb 2524  dfiin2 2584  ssiun 2588  ssiin 2595  axrep1 2690  dffr2 2915  dfepfr 2928  dffr3 3427  asymref2 3436  fun11 3558  f1fv 3869  inf2 4591  axinf2 4607  aceq1 4712  aceq0 4713  axac 4728  ac6n 4740  kmlem14 4761  aceqkm 4764  zfcndrep 4949  zfcndac 4954  primet 6152  raluz2 6388  cau3ir 6867  clm1 7030  climshft 7057  climres 7058  caucvg 7116  islp2 7707  sncld 7747  lmbr2 7891  iscau2 7899  metcnp4 7932  bcthlem7 7967  nmobndseqi 8400  axgroth4 8735  grothprim 8738  cvnbtwn3t 10171  elat2 10223  anidmdbi 10392

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