Theorem imbi1i 341

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	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi1i	⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		imbi1 339	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  ancomst  458  imor  884  ifpn  1099  eximal  1881  19.43  1985  19.37v  2096  19.37  2275  dfsb3  2505  sbrim  2527  sbor  2529  mo4f  2636  mo4fOLD  2637  2mos  2732  neor  3090  r3al  3149  r19.23t  3230  r19.23v  3232  r19.43  3303  ceqsralt  3446  ralab  3590  ralrab  3591  euind  3618  reu2  3619  rmo4  3624  rmo3f  3628  rmo4f  3629  reuind  3638  2reu5lem3  3642  rmo3  3752  dfdif3  3947  raldifb  3977  unss  4014  ralunb  4021  inssdif0  4177  ssundif  4275  dfif2  4308  pwss  4395  ralsnsg  4436  disjsn  4465  snssg  4534  raldifsni  4544  raldifsnb  4545  unissb  4691  intun  4729  intpr  4730  dfiin2g  4773  disjor  4855  dftr2  4977  axrep1  4995  axpweq  5064  zfpow  5066  axpow2  5067  reusv2lem4  5101  reusv2  5103  raliunxp  5494  idrefALT  5750  asymref2  5755  dffun2  6133  dffun4  6135  dffun5  6136  dffun7  6150  fununi  6197  fvn0ssdmfun  6599  dff13  6767  dff14b  6783  zfun  7210  uniex2  7212  dfom2  7328  fimaxg  8476  fiint  8506  dfsup2  8619  fiming  8673  oemapso  8856  scottexs  9027  scott0s  9028  iscard2  9115  acnnum  9188  dfac9  9273  dfacacn  9278  kmlem4  9290  kmlem12  9298  axpowndlem3  9736  zfcndun  9752  zfcndpow  9753  zfcndac  9756  axgroth5  9961  grothpw  9963  axgroth6  9965  addsrmo  10210  mulsrmo  10211  infm3  11312  raluz2  12019  nnwos  12038  ralrp  12134  cotr2g  14094  lo1resb  14672  rlimresb  14673  o1resb  14674  modfsummod  14900  isprm4  15769  acsfn1  16674  acsfn2  16676  lublecllem  17341  isirred2  19055  isdomn2  19660  iunocv  20388  ist1-2  21522  isnrm2  21533  dfconn2  21593  alexsubALTlem3  22223  ismbl  23692  dyadmbllem  23765  ellimc3  24042  dchrelbas2  25375  dchrelbas3  25376  isch2  28624  choc0  28729  h1dei  28953  mdsl2i  29725  disjorf  29928  bnj1101  31390  bnj1109  31392  bnj1533  31457  bnj580  31518  bnj864  31527  bnj865  31528  bnj978  31554  bnj1049  31577  bnj1090  31582  bnj1145  31596  axextprim  32111  axunprim  32113  axpowprim  32114  untuni  32119  3orit  32129  biimpexp  32130  elintfv  32193  dfon2lem8  32222  soseq  32282  dfom5b  32547  bj-axrep1  33306  bj-zfpow  33313  bj-raldifsn  33570  rdgeqoa  33756  wl-equsalcom  33865  poimirlem25  33971  poimirlem30  33976  tsim1  34470  inxpss  34624  idinxpss  34625  idinxpssinxp  34629  ineleq  34660  cocossss  34732  cosscnvssid3  34767  trcoss2  34775  eqvrelcoels4  34903  redpbi1  34913  cvlsupr3  35412  pmapglbx  35837  isltrn2N  36188  cdlemefrs29bpre0  36464  fphpd  38217  dford4  38432  fnwe2lem2  38457  isdomn3  38618  ifpidg  38671  ifpid1g  38674  ifpor123g  38688  undmrnresiss  38744  elintima  38779  df3or2  38894  dfhe3  38902  dffrege76  39066  dffrege115  39105  frege131  39121  ntrneikb  39225  ntrneixb  39226  pm14.12  39454  dfvd2an  39619  dfvd3  39628  dfvd3an  39631  uun2221  39860  uun2221p1  39861  uun2221p2  39862  disjinfi  40181  supxrleubrnmptf  40468  fsummulc1f  40590  fsumiunss  40595  fnlimfvre2  40697  limsupreuz  40757  limsupvaluz2  40758  dvmptmulf  40940  dvnmul  40946  dvmptfprodlem  40947  dvnprodlem2  40950  sge0ltfirpmpt2  41427  hoidmv1le  41595  hoidmvle  41601  vonioolem2  41682  smflimlem3  41768  setrec2  43330  aacllem  43436