Theorem imbi1i 161

Description: Introduce a consequent to both sides of a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		bi.a	. . . 4 |- (ph <-> ps)
2	1	biimpr 134	. . 3 |- (ps -> ph)
3	2	syl4 19	. 2 |- ((ph -> ch) -> (ps -> ch))
4	1	biimp 133	. . 3 |- (ph -> ps)
5	4	syl4 19	. 2 |- ((ps -> ch) -> (ph -> ch))
6	3, 5	impbi 139	1 |- ((ph -> ch) <-> (ps -> ch))

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

This theorem is referenced by:  imbi12i 163  imor 204  impexp 276  bibi2i 460  19.37 759  sbor 887  sb19.21 888  mo4f 1028  axun 1081  axpow 1082  r3al 1240  r19.23v 1282  ralcom 1312  reu2 1338  reu4 1340  unss 1632  inssdif0 1754  pwex 1806  snss 1849  unissb 1941  uniex 1947  intun 1989  intpr 1990  dfiin2 2015  iunss 2017  dftr2 2043  dfom2 2374  reluni 2493  dffun2 2674  dffun4 2676  dffun5 2677  dffun6 2687  fununi 2705  funcnvuni 2706  f1fv 2916  setind2 3493  ranksn 3532  scottexs 3543  scott0s 3544  kardex 3550  karden 3551  kmlem11 3590  axpowndlem3 3745  zfcndun 3761  zfcndpow 3762  zfcndac 3765  suppsr3 4018  nnwos 4610  zmin 4617  choc0 5291  h1deot 5454  h1det 5455

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