Theorem imbi1i 331

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

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

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 190

This theorem is referenced by:  imor  418  ancomst  458  ifpn  1445  eximal  1676  19.43  1755  19.37v  1836  19.37  2056  dfsb3  2213  sbrim  2235  sbor  2237  mo4f  2355  2mos  2391  neor  2726  r3al  2779  r3alOLD  2837  r19.23t  2876  r19.23v  2878  r19.43  2957  ceqsralt  3082  ralab  3210  ralrab  3211  euind  3236  reu2  3237  rmo4  3242  reuind  3254  2reu5lem3  3258  rmo3  3369  raldifb  3584  unss  3619  ralunb  3626  inssdif0  3845  ssundif  3862  dfif2  3894  pwss  3977  ralsnsg  4014  disjsn  4043  snss  4108  raldifsni  4114  raldifsnb  4115  unissb  4242  intun  4280  intpr  4281  dfiin2g  4324  disjor  4400  dftr2  4512  axrep1  4529  axpweq  4593  zfpow  4595  axpow2  4596  reusv2lem4  4620  reusv2  4622  raliunxp  4992  asymref2  5235  dffun2  5610  dffun4  5612  dffun5  5613  dffun7  5626  fununi  5670  fvn0ssdmfun  6035  dff13  6183  dff14b  6195  zfun  6610  uniex2  6612  dfom2  6720  fimaxg  7843  fiint  7873  dfsup2  7983  fiming  8039  oemapso  8212  scottexs  8383  scott0s  8384  iscard2  8435  acnnum  8508  dfac9  8591  dfacacn  8596  kmlem4  8608  kmlem12  8616  axpowndlem3  9049  zfcndun  9065  zfcndpow  9066  zfcndac  9069  axgroth5  9274  grothpw  9276  axgroth6  9278  addsrmo  9522  mulsrmo  9523  infm3  10595  raluz2  11236  nnwos  11254  ralrp  11349  cotr2g  13088  lo1resb  13676  rlimresb  13677  o1resb  13678  modfsummod  13902  isprm4  14682  acsfn1  15615  acsfn2  15617  lublecllem  16282  isirred2  17977  isdomn2  18571  iunocv  19292  ist1-2  20411  isnrm2  20422  dfcon2  20482  alexsubALTlem3  21112  ismbl  22528  dyadmbllem  22605  ellimc3  22882  dchrelbas2  24213  dchrelbas3  24214  isch2  26924  choc0  27027  h1dei  27251  mdsl2i  28023  rmo3f  28179  rmo4fOLD  28180  rmo4f  28181  disjorf  28237  bnj538OLD  29598  bnj1101  29644  bnj1109  29646  bnj1533  29711  bnj580  29772  bnj864  29781  bnj865  29782  bnj978  29808  bnj1049  29831  bnj1090  29836  bnj1145  29850  axextprim  30376  axunprim  30378  axpowprim  30379  untuni  30384  3orit  30395  biimpexp  30396  dfon2lem8  30484  soseq  30540  dfom5b  30727  bj-axrep1  31447  bj-zfpow  31454  rdgeqoa  31817  wl-equsalcom  31919  poimirlem25  32009  poimirlem30  32014  tsim1  32416  cvlsupr3  32954  pmapglbx  33378  isltrn2N  33729  cdlemefrs29bpre0  34007  fphpd  35703  dford4  35928  fnwe2lem2  35953  isdomn3  36125  ifpidg  36179  ifpid1g  36182  ifpor123g  36196  undmrnresiss  36254  elintima  36289  df3or2  36404  dfhe3  36414  dffrege76  36579  dffrege115  36618  frege131  36634  pm14.12  36815  dfvd2an  36994  dfvd3  37003  dfvd3an  37006  uun2221  37239  uun2221p1  37240  uun2221p2  37241  disjinfi  37505  fsummulc1f  37684  fsumiunss  37691  dvmptmulf  37849  dvnmul  37855  dvmptfprodlem  37856  dvnprodlem2  37859  sge0ltfirpmpt2  38305  hoidmv1le  38453  hoidmvle  38459  aacllem  40812