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 610  19.37 1082  dfsb3 1228  sbor 1237  sb19.21 1238  a12lem2 1379  mo4f 1404  2mos 1451  neor 1641  r3al 1693  r19.23v 1744  ralcom 1777  reu2 1933  rmo4 1936  unss 2208  inssdif0 2338  ssundif 2349  dfif2 2368  ralpr 2433  snss 2466  unissb 2533  ssintab 2555  intun 2567  intpr 2568  dfiin2 2593  iunss 2596  dftr2 2688  axpow 2750  pwex 2752  sbcsng 2760  axun 2874  uniex2 2876  dfom2 3140  reluni 3272  asymref2 3447  dffun2 3533  dffun4 3535  dffun5 3536  dffun6 3546  fununi 3570  funcnvuni 3571  f1fv 3881  fiint 4576  fiintOLD 4577  setind2 4666  ranksn 4706  scottexs 4735  scott0s 4736  kardex 4742  karden 4743  kmlem4 4785  kmlem12 4793  axpowndlem3 4970  zfcndun 4986  zfcndpow 4987  zfcndac 4990  suppsr3 5243  infm3 6063  infmsup 6077  zmin 6228  ralrp 6297  raluz2 6451  nnwos 6468  clm4 7087  ntreq0 7712  islp2 7751  cncfmet 7909  spwpr2 8661  choc0 9292  h1deot 9474  h1det 9475  mdsl2 10252

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