Theorem imbi1i 325

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbi1i.1	|- ( ph <-> ps )

Assertion

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

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 |- ( ph <-> ps )
2		imbi1 323	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 5	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

Syntax hints:   -> wi 4   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  imor  412  ancomst  452  19.43  1665  19.37  1910  dfsb3  2081  sbrim  2104  sbor  2106  sbcom2  2166  mo4f  2331  2mos  2378  neor  2784  r3al  2837  r3alOLD  2895  r19.23t  2934  r19.23v  2936  r19.43  3010  ceqsralt  3130  ralab  3257  ralrab  3258  euind  3283  reu2  3284  rmo4  3289  reuind  3300  2reu5lem3  3304  rmo3  3423  raldifb  3637  unss  3671  ralunb  3678  inssdif0  3887  ssundif  3903  dfif2  3934  pwss  4018  ralsnsg  4052  disjsn  4081  snss  4144  raldifsni  4150  raldifsnb  4151  unissb  4270  intun  4307  intpr  4308  dfiin2g  4351  disjor  4424  dftr2  4535  axrep1  4552  axpweq  4617  zfpow  4619  axpow2  4620  reusv2lem4  4644  reusv2  4646  reusv7OLD  4652  raliunxp  5133  asymref2  5375  dffun2  5589  dffun4  5591  dffun5  5592  dffun7  5605  fununi  5645  dff13  6145  dff14b  6157  zfun  6568  uniex2  6570  dfom2  6673  fimaxg  7756  fiint  7786  dfsup2  7891  oemapso  8090  scottexs  8294  scott0s  8295  iscard2  8346  acnnum  8422  dfac9  8505  dfacacn  8510  kmlem4  8522  kmlem12  8530  axpowndlem3  8964  axpowndlem3OLD  8965  zfcndun  8982  zfcndpow  8983  zfcndac  8986  axgroth5  9191  grothpw  9193  axgroth6  9195  addsrmo  9439  mulsrmo  9440  infm3  10491  raluz2  11119  nnwos  11138  ralrp  11227  lo1resb  13336  rlimresb  13337  o1resb  13338  modfsummod  13557  isprm4  14075  acsfn1  14905  acsfn2  14907  lublecllem  15464  isirred2  17127  isdomn2  17712  iunocv  18472  fvmptnn04if  19110  ist1-2  19607  isnrm2  19618  dfcon2  19679  alexsubALTlem3  20277  ismbl  21665  dyadmbllem  21736  ellimc3  22011  dchrelbas2  23233  dchrelbas3  23234  legov  23692  eengtrkg  23957  isch2  25803  choc0  25906  h1dei  26130  mdsl2i  26903  xfree2  27026  spc2ed  27034  rmo3f  27056  rmo4fOLD  27057  rmo4f  27058  disjorf  27099  axextprim  28534  axunprim  28536  axpowprim  28537  untuni  28542  3orit  28553  biimpexp  28554  dfon2lem8  28785  predreseq  28822  soseq  28897  dfom5b  29125  wl-equsalcom  29558  wl-sbcom2d  29574  tsim1  30128  fphpd  30341  dford4  30564  fnwe2lem2  30590  isdomn3  30758  pm14.12  30861  ellimcabssub0  31114  sumnnodd  31127  volioc  31245  dirkercncflem2  31359  fourierdlem32  31394  fourierdlem49  31411  fourierdlem81  31443  fourierdlem83  31445  dfvd2an  32314  dfvd3  32323  dfvd3an  32326  uun2221  32565  uun2221p1  32566  uun2221p2  32567  bnj538  32751  bnj1101  32797  bnj1109  32799  bnj1533  32864  bnj580  32925  bnj864  32934  bnj865  32935  bnj978  32961  bnj1049  32984  bnj1090  32989  bnj1145  33003  bj-ifn  33111  bj-eximal  33151  bj-axrep1  33330  bj-zfpow  33337  cvlsupr3  34016  pmapglbx  34440  isltrn2N  34791  cdlemefrs29bpre0  35067