Theorem imbi1i 184

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	biimpri 150	. . 3 |- (ps -> ph)
3	2	imim1i 16	. 2 |- ((ph -> ch) -> (ps -> ch))
4	1	biimpi 149	. . 3 |- (ph -> ps)
5	4	imim1i 16	. 2 |- ((ps -> ch) -> (ph -> ch))
6	3, 5	impbii 155	1 |- ((ph -> ch) <-> (ps -> ch))

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

This theorem is referenced by:  imbi12i 186  imor 232  impexp 345  pm4.78 352  bibi2i 611  19.37 1116  dfsb3 1263  sbor 1272  sb19.21 1273  a12lem2 1416  mo4f 1441  2mos 1488  neor 1684  r3al 1736  r19.23v 1787  ralcom 1820  reu2 1976  rmo4 1979  sbc2ie 2036  unss 2256  inssdif0 2386  ssundif 2398  dfif2 2417  pwss 2466  ralpr 2486  ralsng 2489  sbcsng 2490  snss 2525  unissb 2595  ssintab 2617  intun 2629  intpr 2630  dfiin2 2656  iunss 2659  dftr2 2756  axpweq 2817  zfpow 2819  axpow2 2820  pwex 2823  zfun 3090  uniex2 3092  dfom2 3220  asymref2 3532  dffun2 3631  dffun4 3633  dffun5 3634  dffun7 3644  fununi 3668  funcnvuni 3669  dff13 3988  ac6sfi 4591  fiint 4703  setind2 4795  ranksn 4835  scottexs 4864  scott0s 4865  kardex 4871  karden 4872  kmlem4 4914  kmlem12 4922  axpowndlem3 5105  zfcndun 5121  zfcndpow 5122  zfcndac 5125  suppsr3 5378  ralrp 6205  infm3 6222  infmsup 6236  zmin 6391  raluz2 6570  nnwos 6587  clm4i 7283  ntreq0 7918  islp2 7957  cncfmet 8116  spwpr2 8920  grothpw 9054  axgroth5 9055  choc0 9566  h1deoi 9748  h1dei 9749  mdsl2i 10530  xfree2 10654  domrngref 10764  isexid 10893  dfiin2g 11400  compfipin0 11493  alexsublem3 11498  alexsublem4 11499  neibastop2 11584  neibastop3 11585  fbssint 11626  gapm 11784  heiborlem13 12023  heiborlem16 12026

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 145

Copyright terms: Public domain