Theorem imbi2i 160

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 133	. . 3 |- (ph -> ps)
3	2	syl3 18	. 2 |- ((ch -> ph) -> (ch -> ps))
4	1	biimpr 134	. . 3 |- (ps -> ph)
5	4	syl3 18	. 2 |- ((ch -> ps) -> (ch -> ph))
6	3, 5	impbi 139	1 |- ((ch -> ph) <-> (ch -> ps))

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

This theorem is referenced by:  imbi12i 163  iman 205  orbi2i 214  or12 217  anass 336  bibi2i 460  pm5.32 488  oibabs 493  orcana 509  nan 514  19.35 754  19.36 757  sban 889  eu1 1019  moabs 1041  moanim 1051  axac 1085  r2al 1231  r19.21v 1260  r19.35 1298  ralcom2 1314  reu2 1338  ssconb 1598  disj2 1735  inssdif0 1754  pwpw0 1883  unissb 1941  dfiin2 2015  ssiun 2018  ssiin 2024  dffr2 2171  dfepfr 2184  dffr3 2620  f1fv 2916  inf2 3459  inf4 3473  aceq1 3552  aceq0 3553  kmlem4 3583  kmlem14 3593  zfcndrep 3760  zfcndac 3765  cvnbtwn3t 5720  elat2 5739

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

metamath.org