Theorem imbi1i 186

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 152	. . 3 |- (ps -> ph)
3	2	imim1i 16	. 2 |- ((ph -> ch) -> (ps -> ch))
4	1	biimp 151	. . 3 |- (ph -> ps)
5	4	imim1i 16	. 2 |- ((ps -> ch) -> (ph -> ch))
6	3, 5	impbi 157	1 |- ((ph -> ch) <-> (ps -> ch))

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

This theorem is referenced by:  imbi12i 188  imor 234  impexp 347  pm4.78 354  bibi2i 608  19.37 1080  dfsb3 1226  sbor 1235  sb19.21 1236  a12lem2 1377  mo4f 1402  2mos 1448  neor 1638  r3al 1690  r19.23v 1741  ralcom 1774  reu2 1930  rmo4 1933  unss 2204  inssdif0 2333  ssundif 2344  dfif2 2363  ralpr 2428  snss 2461  unissb 2528  ssintab 2550  intun 2562  intpr 2563  dfiin2 2588  iunss 2591  dftr2 2682  axpow 2743  pwex 2745  sbcsng 2753  axun 2867  uniex2 2869  dfom2 3133  reluni 3265  asymref2 3440  dffun2 3526  dffun4 3528  dffun5 3529  dffun6 3539  fununi 3563  funcnvuni 3564  f1fv 3874  fiint 4559  fiintOLD 4560  setind2 4649  ranksn 4689  scottexs 4718  scott0s 4719  kardex 4725  karden 4726  kmlem4 4768  kmlem12 4776  axpowndlem3 4951  zfcndun 4967  zfcndpow 4968  zfcndac 4971  suppsr3 5224  infm3 6054  infmsup 6068  zmin 6219  ralrp 6289  raluz2 6443  nnwos 6460  clm4 7080  ntreq0 7708  islp2 7747  cncfmet 7905  spwpr2 8658  choc0 9290  h1deot 9472  h1det 9473  mdsl2 10249

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