Theorem biimpa 294

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpa	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  simprbda  380  simplbda  381  pm5.1  590  bimsc1  947  biimp3a  1323  equsex  1706  euor  2023  euan  2053  cgsexg  2716  cgsex2g  2717  cgsex4g  2718  ceqsex  2719  sbciegft  2934  sbeqalb  2960  sseqtrid  3142  exmidn0m  4119  euotd  4171  ralxfr2d  4380  rexxfr2d  4381  nlimsucg  4476  wetriext  4486  relop  4684  resiexg  4859  iotass  5100  fnbr  5220  f1o00  5395  fnex  5635  foelrn  5647  acexmidlemab  5761  f1ocnv2d  5967  ofrval  5985  eloprabi  6087  1stconst  6111  2ndconst  6112  poxp  6122  smodm2  6185  smoiso  6192  nnsucuniel  6384  erth  6466  iinerm  6494  phplem4dom  6749  findcard2  6776  findcard2s  6777  fimax2gtrilemstep  6787  undifdcss  6804  fipwssg  6860  supelti  6882  nlt1pig  7142  dfplpq2  7155  ltsonq  7199  archnqq  7218  nqnq0pi  7239  prarloclemn  7300  genprndl  7322  genprndu  7323  genpdisj  7324  addlocprlemgt  7335  addlocpr  7337  nqprl  7352  nqpru  7353  addnqprlemrl  7358  addnqprlemru  7359  mulnqprlemrl  7374  mulnqprlemru  7375  ltpopr  7396  ltexprlemloc  7408  ltexprlemrl  7411  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  caucvgprlemladdfu  7478  suplocexprlemru  7520  axcaucvglemres  7700  cnegex  7933  mullt0  8235  eqord1  8238  mulge0  8374  divap0  8437  div2negap  8488  prodgt0  8603  ltmul12a  8611  recgt1i  8649  div4p1lem1div2  8966  nn0lt2  9125  peano5uzti  9152  btwnapz  9174  eluzp1m1  9342  eluzaddi  9345  eluzsubi  9346  uz2m1nn  9392  rphalflt  9464  xleaddadd  9663  ixxdisj  9679  iccgelb  9708  icodisj  9768  iccf1o  9780  fzsuc2  9852  fzonmapblen  9957  flqge0nn0  10059  flqge1nn  10060  modfzo0difsn  10161  expubnd  10343  bernneq  10405  bernneq2  10406  nn0opthlem2d  10460  facwordi  10479  bcpasc  10505  hashnncl  10535  recvguniq  10760  sqrt0rlem  10768  resqrexlemover  10775  resqrexlemcalc3  10781  resqrexlemgt0  10785  resqrexlemoverl  10786  recvalap  10862  nnabscl  10865  negfi  10992  climi0  11051  climge0  11087  summodclem3  11142  fsumsplit  11169  fisumcom2  11200  fisumrev2  11208  explecnv  11267  cvgratnnlemseq  11288  eftlub  11385  sin02gt0  11459  dvdslelemd  11530  dvdsleabs2  11533  mulmoddvds  11550  odd2np1  11559  oexpneg  11563  mod2eq1n2dvds  11565  sqoddm1div8z  11572  zsupcllemstep  11627  rplpwr  11704  rppwr  11705  nn0seqcvgd  11711  lcmneg  11744  qredeq  11766  dvdsnprmd  11795  oddprmge3  11804  oddpwdclemdvds  11837  oddpwdclemndvds  11838  oddpwdclemodd  11839  znege1  11845  qgt0numnn  11866  phibndlem  11881  hashgcdeq  11893  ennnfonelemf1  11920  neiuni  12319  neissex  12323  tgrest  12327  tgcnp  12367  lmfpm  12401  lmcl  12403  lmss  12404  lmff  12407  psmetdmdm  12482  xmeter  12594  neibl  12649  xmettxlem  12667  tgqioo  12705  cnopnap  12752  limcimo  12792  sinq12gt0  12900  isomninnlem  13214