Theorem imbi1i 203

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 169	. . 3 |- (ps -> ph)
3	2	imim1i 19	. 2 |- ((ph -> ch) -> (ps -> ch))
4	1	biimpi 168	. . 3 |- (ph -> ps)
5	4	imim1i 19	. 2 |- ((ps -> ch) -> (ph -> ch))
6	3, 5	impbii 174	1 |- ((ph -> ch) <-> (ps -> ch))

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

This theorem is referenced by:  imbi12i 205  imor 251  impexp 374  pm4.78 381  bibi2i 669  bibi2iOLD 670  ancomsimp 1291  19.37 1431  dfsb3 1596  sbor 1605  sb19.21 1606  a12lem2 1768  mo4f 1798  2mos 1852  neor 2096  r3al 2151  r19.23 2206  r19.23OLD 2207  r19.43 2238  ralcom 2242  ralab 2417  euind 2439  reu2 2442  rmo4 2445  reuind 2450  sbc2ie 2523  unss 2780  ralunb 2784  inssdif0 2940  inssdif0OLD 2941  ssundif 2955  dfif2 2984  pwss 3043  ralprg 3078  ralprOLD 3080  ralprOLDOLD 3081  raltp 3083  ralsng 3085  sbcsngOLD 3087  disjsn 3089  snss 3122  unissb 3208  ssintabOLD 3234  intun 3249  intpr 3250  dfiin2g 3286  dfiin2OLD 3288  iunssOLD 3292  iinxsng 3325  iinxprg 3326  dftr2 3413  truni 3425  axpweq 3480  zfpow 3482  axpow2 3483  pwexOLD 3488  zfun 3791  uniex2 3793  eufromeq4 3831  dfom2 3951  asymref2 4310  asymref2OLD 4311  dffun2 4431  dffun4 4433  dffun5 4434  dffun7 4447  fununi 4481  dff13 4850  ac6sfi 5509  fiint 5650  setind2 5760  ranksn 5800  scottexs 5848  scott0s 5849  kmlem4 5930  kmlem12 5938  axpowndlem3 6103  zfcndun 6119  zfcndpow 6120  zfcndac 6123  suppsr3 6376  ralrp 7246  infm3 7263  infmsup 7277  zmin 7432  raluz2 7612  nnwos 7629  clm4i 8340  ntreq0 8984  islp2 9023  cncfmet 9183  gapm 9462  spwpr2 10001  axgroth5 10132  grothpw 10134  axgroth6 10137  fbssint 10279  isexid 10364  choc0 10923  h1deoi 11105  h1dei 11106  mdsl2i 11894  xfree2 12017  bnj45 12415  bnj538 12534  bnj856 12789  bnj857 12790  bnj861 12794  bnj869 12797  bnj980 12862  bnj979 12863  bnj1050 12889  bnj1055 12892  bnj1074 12903  bnj1079 12906  bnj1086 12908  bnj1088 12910  bnj1089 12911  bnj1101 12918  bnj1120 12930  bnj1508 13168  bnj1509 13169  bnj86 13213  bnj87 13214  bnj582 13295  bnj580 13301  bnj1049 13394  bnj1062 13397  bnj1067 13399  bnj1070 13401  bnj1077 13405  bnj1090 13410  3prm 13780  axextprim 13785  axunprim 13787  axpowprim 13788  truniOLD 13792  untuni 13797  3orit 13811  biimpexp 13815  ralunbOLD 13819  dfon2lem8 13856  predreseq 13890  trclss 13935  soseq 13955  dfom5 14081  fates 14292  nxtor 14312  domrngref 14364  trooo 14758  vecval1b 14794  bpmp 15251  btmp 15252  dfiin2gOLD 15356  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  neibastop2 15523  neibastop3 15524  ralabOLD 15669  fimax2g 15769  frminex 15773  heiborlem13 15967  heiborlem16 15970  conss1 16421  dfvd3 16495  lubid 16807  pmapglbx 17251

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 164

Copyright terms: Public domain