Theorem imbi1i 326

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 324	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 5	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

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

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 188

This theorem is referenced by:  imor  413  ancomst  453  ifpn  1430  eximal  1662  19.43  1737  19.37v  1815  19.37  2020  dfsb3  2166  sbrim  2188  sbor  2190  mo4f  2310  2mos  2347  neor  2746  r3al  2803  r3alOLD  2861  r19.23t  2901  r19.23v  2903  r19.43  2982  ceqsralt  3102  ralab  3229  ralrab  3230  euind  3255  reu2  3256  rmo4  3261  reuind  3272  2reu5lem3  3276  rmo3  3387  raldifb  3602  unss  3637  ralunb  3644  inssdif0  3859  ssundif  3876  dfif2  3908  pwss  3991  ralsnsg  4025  disjsn  4054  snss  4118  raldifsni  4124  raldifsnb  4125  unissb  4244  intun  4282  intpr  4283  dfiin2g  4326  disjor  4402  dftr2  4513  axrep1  4530  axpweq  4593  zfpow  4595  axpow2  4596  reusv2lem4  4620  reusv2  4622  raliunxp  4985  asymref2  5228  dffun2  5602  dffun4  5604  dffun5  5605  dffun7  5618  fununi  5658  fvn0ssdmfun  6019  dff13  6165  dff14b  6177  zfun  6589  uniex2  6591  dfom2  6699  fimaxg  7815  fiint  7845  dfsup2  7955  oemapso  8177  scottexs  8348  scott0s  8349  iscard2  8400  acnnum  8472  dfac9  8555  dfacacn  8560  kmlem4  8572  kmlem12  8580  axpowndlem3  9013  zfcndun  9029  zfcndpow  9030  zfcndac  9033  axgroth5  9238  grothpw  9240  axgroth6  9242  addsrmo  9486  mulsrmo  9487  infm3  10557  raluz2  11197  nnwos  11215  ralrp  11310  cotr2g  13008  lo1resb  13595  rlimresb  13596  o1resb  13597  modfsummod  13821  isprm4  14594  acsfn1  15511  acsfn2  15513  lublecllem  16178  isirred2  17857  isdomn2  18451  iunocv  19168  ist1-2  20287  isnrm2  20298  dfcon2  20358  alexsubALTlem3  20988  ismbl  22354  dyadmbllem  22431  ellimc3  22708  dchrelbas2  24025  dchrelbas3  24026  isch2  26708  choc0  26811  h1dei  27035  mdsl2i  27807  rmo3f  27963  rmo4fOLD  27964  rmo4f  27965  disjorf  28025  bnj538OLD  29335  bnj1101  29381  bnj1109  29383  bnj1533  29448  bnj580  29509  bnj864  29518  bnj865  29519  bnj978  29545  bnj1049  29568  bnj1090  29573  bnj1145  29587  axextprim  30113  axunprim  30115  axpowprim  30116  untuni  30121  3orit  30132  biimpexp  30133  dfon2lem8  30220  soseq  30276  dfom5b  30461  bj-axrep1  31151  bj-zfpow  31158  wl-equsalcom  31579  poimirlem25  31669  poimirlem30  31674  tsim1  32076  cvlsupr3  32619  pmapglbx  33043  isltrn2N  33394  cdlemefrs29bpre0  33672  fphpd  35368  dford4  35594  fnwe2lem2  35619  isdomn3  35784  ifpidg  35838  ifpid1g  35841  ifpor123g  35855  elintima  35888  dfhe3  36011  dffrege76  36176  dffrege115  36215  frege131  36231  pm14.12  36413  dfvd2an  36594  dfvd3  36603  dfvd3an  36606  uun2221  36844  uun2221p1  36845  uun2221p2  36846  disjinfi  37095  fsummulc1f  37226  fsumiunss  37233  dvmptmulf  37385  dvnmul  37391  dvmptfprodlem  37392  dvnprodlem2  37395  aacllem  39314