Theorem imbi1i 339

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 337	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  imor  428  ancomst  468  ifpn  1021  eximal  1704  19.43  1807  19.37v  1907  19.37  2098  dfsb3  2373  sbrim  2395  sbor  2397  mo4f  2515  2mos  2551  neor  2881  r3al  2936  r19.23t  3016  r19.23v  3018  r19.43  3087  ceqsralt  3219  ralab  3354  ralrab  3355  euind  3380  reu2  3381  rmo4  3386  reuind  3398  2reu5lem3  3402  rmo3  3514  raldifb  3734  unss  3771  ralunb  3778  inssdif0  3927  dfnf5  3932  ssundif  4030  dfif2  4066  pwss  4153  ralsnsg  4194  disjsn  4223  snss  4293  raldifsni  4300  raldifsnb  4301  unissb  4442  intun  4481  intpr  4482  dfiin2g  4526  disjor  4607  dftr2  4724  axrep1  4742  axpweq  4812  zfpow  4814  axpow2  4815  reusv2lem4  4842  reusv2  4844  raliunxp  5231  asymref2  5482  dffun2  5867  dffun4  5869  dffun5  5870  dffun7  5884  fununi  5932  fvn0ssdmfun  6316  dff13  6477  dff14b  6493  zfun  6915  uniex2  6917  dfom2  7029  fimaxg  8167  fiint  8197  dfsup2  8310  fiming  8364  oemapso  8539  scottexs  8710  scott0s  8711  iscard2  8762  acnnum  8835  dfac9  8918  dfacacn  8923  kmlem4  8935  kmlem12  8943  axpowndlem3  9381  zfcndun  9397  zfcndpow  9398  zfcndac  9401  axgroth5  9606  grothpw  9608  axgroth6  9610  addsrmo  9854  mulsrmo  9855  infm3  10942  raluz2  11697  nnwos  11715  ralrp  11812  cotr2g  13665  lo1resb  14245  rlimresb  14246  o1resb  14247  modfsummod  14472  isprm4  15340  acsfn1  16262  acsfn2  16264  lublecllem  16928  isirred2  18641  isdomn2  19239  iunocv  19965  ist1-2  21091  isnrm2  21102  dfconn2  21162  alexsubALTlem3  21793  ismbl  23234  dyadmbllem  23307  ellimc3  23583  dchrelbas2  24896  dchrelbas3  24897  isch2  27968  choc0  28073  h1dei  28297  mdsl2i  29069  rmo3f  29224  rmo4fOLD  29225  rmo4f  29226  disjorf  29278  bnj538OLD  30571  bnj1101  30616  bnj1109  30618  bnj1533  30683  bnj580  30744  bnj864  30753  bnj865  30754  bnj978  30780  bnj1049  30803  bnj1090  30808  bnj1145  30822  axextprim  31339  axunprim  31341  axpowprim  31342  untuni  31347  3orit  31358  biimpexp  31359  dfon2lem8  31449  soseq  31505  dfom5b  31714  bj-axrep1  32484  bj-zfpow  32491  rdgeqoa  32889  wl-equsalcom  32999  poimirlem25  33105  poimirlem30  33110  tsim1  33608  cvlsupr3  34150  pmapglbx  34574  isltrn2N  34925  cdlemefrs29bpre0  35203  fphpd  36899  dford4  37115  fnwe2lem2  37140  isdomn3  37302  ifpidg  37356  ifpid1g  37359  ifpor123g  37373  undmrnresiss  37430  elintima  37465  df3or2  37580  dfhe3  37590  dffrege76  37754  dffrege115  37793  frege131  37809  ntrneikb  37913  ntrneixb  37914  pm14.12  38143  dfvd2an  38319  dfvd3  38328  dfvd3an  38331  uun2221  38561  uun2221p1  38562  uun2221p2  38563  disjinfi  38889  fsummulc1f  39238  fsumiunss  39243  fnlimfvre2  39345  limsupreuz  39405  limsupvaluz2  39406  dvmptmulf  39489  dvnmul  39495  dvmptfprodlem  39496  dvnprodlem2  39499  sge0ltfirpmpt2  39980  hoidmv1le  40145  hoidmvle  40151  vonioolem2  40232  smflimlem3  40318  setrec2  41765  aacllem  41880