Theorem imbi1i 338

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 336	. 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  427  ancomst  467  ifpn  1060  eximal  1856  19.43  1959  19.37v  2075  19.37  2247  dfsb3  2511  sbrim  2533  sbor  2535  mo4f  2654  2mos  2690  neor  3023  r3al  3078  r19.23t  3159  r19.23v  3161  r19.43  3231  ceqsralt  3369  ralab  3508  ralrab  3509  euind  3534  reu2  3535  rmo4  3540  reuind  3552  2reu5lem3  3556  rmo3  3669  dfdif3  3863  raldifb  3893  unss  3930  ralunb  3937  inssdif0  4090  dfnf5  4095  ssundif  4196  dfif2  4232  pwss  4319  ralsnsg  4360  disjsn  4390  snssg  4459  raldifsni  4470  raldifsnb  4471  unissb  4621  intun  4661  intpr  4662  dfiin2g  4705  disjor  4786  dftr2  4906  axrep1  4924  axpweq  4991  zfpow  4993  axpow2  4994  reusv2lem4  5021  reusv2  5023  raliunxp  5417  asymref2  5671  dffun2  6059  dffun4  6061  dffun5  6062  dffun7  6076  fununi  6125  fvn0ssdmfun  6514  dff13  6676  dff14b  6692  zfun  7116  uniex2  7118  dfom2  7233  fimaxg  8374  fiint  8404  dfsup2  8517  fiming  8571  oemapso  8754  scottexs  8925  scott0s  8926  iscard2  9012  acnnum  9085  dfac9  9170  dfacacn  9175  kmlem4  9187  kmlem12  9195  axpowndlem3  9633  zfcndun  9649  zfcndpow  9650  zfcndac  9653  axgroth5  9858  grothpw  9860  axgroth6  9862  addsrmo  10106  mulsrmo  10107  infm3  11194  raluz2  11950  nnwos  11968  ralrp  12065  cotr2g  13936  lo1resb  14514  rlimresb  14515  o1resb  14516  modfsummod  14745  isprm4  15619  acsfn1  16543  acsfn2  16545  lublecllem  17209  isirred2  18921  isdomn2  19521  iunocv  20247  ist1-2  21373  isnrm2  21384  dfconn2  21444  alexsubALTlem3  22074  ismbl  23514  dyadmbllem  23587  ellimc3  23862  dchrelbas2  25182  dchrelbas3  25183  isch2  28410  choc0  28515  h1dei  28739  mdsl2i  29511  rmo3f  29664  rmo4fOLD  29665  rmo4f  29666  disjorf  29720  bnj538OLD  31138  bnj1101  31183  bnj1109  31185  bnj1533  31250  bnj580  31311  bnj864  31320  bnj865  31321  bnj978  31347  bnj1049  31370  bnj1090  31375  bnj1145  31389  axextprim  31906  axunprim  31908  axpowprim  31909  untuni  31914  3orit  31924  biimpexp  31925  elintfv  31990  dfon2lem8  32021  soseq  32081  dfom5b  32346  bj-axrep1  33116  bj-zfpow  33123  bj-raldifsn  33378  rdgeqoa  33547  wl-equsalcom  33659  poimirlem25  33765  poimirlem30  33770  tsim1  34268  inxpss  34424  idinxpss  34425  idinxpssinxp  34429  ineleq  34460  cocossss  34532  cosscnvssid3  34567  trcoss2  34575  cvlsupr3  35152  pmapglbx  35576  isltrn2N  35927  cdlemefrs29bpre0  36204  fphpd  37900  dford4  38116  fnwe2lem2  38141  isdomn3  38302  ifpidg  38356  ifpid1g  38359  ifpor123g  38373  undmrnresiss  38430  elintima  38465  df3or2  38580  dfhe3  38589  dffrege76  38753  dffrege115  38792  frege131  38808  ntrneikb  38912  ntrneixb  38913  pm14.12  39142  dfvd2an  39318  dfvd3  39327  dfvd3an  39330  uun2221  39560  uun2221p1  39561  uun2221p2  39562  disjinfi  39897  supxrleubrnmptf  40196  fsummulc1f  40323  fsumiunss  40328  fnlimfvre2  40430  limsupreuz  40490  limsupvaluz2  40491  dvmptmulf  40673  dvnmul  40679  dvmptfprodlem  40680  dvnprodlem2  40683  sge0ltfirpmpt2  41164  hoidmv1le  41332  hoidmvle  41338  vonioolem2  41419  smflimlem3  41505  setrec2  42970  aacllem  43078