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  381  simplbda  382  pm5.1  591  bimsc1  948  biimp3a  1324  equsex  1707  euor  2026  euan  2056  cgsexg  2724  cgsex2g  2725  cgsex4g  2726  ceqsex  2727  sbciegft  2943  sbeqalb  2969  sseqtrid  3152  exmidn0m  4132  euotd  4184  ralxfr2d  4393  rexxfr2d  4394  nlimsucg  4489  wetriext  4499  relop  4697  resiexg  4872  iotass  5113  fnbr  5233  f1o00  5410  fnex  5650  foelrn  5662  acexmidlemab  5776  f1ocnv2d  5982  ofrval  6000  eloprabi  6102  1stconst  6126  2ndconst  6127  poxp  6137  smodm2  6200  smoiso  6207  nnsucuniel  6399  erth  6481  iinerm  6509  phplem4dom  6764  findcard2  6791  findcard2s  6792  fimax2gtrilemstep  6802  undifdcss  6819  fipwssg  6875  supelti  6897  nlt1pig  7173  dfplpq2  7186  ltsonq  7230  archnqq  7249  nqnq0pi  7270  prarloclemn  7331  genprndl  7353  genprndu  7354  genpdisj  7355  addlocprlemgt  7366  addlocpr  7368  nqprl  7383  nqpru  7384  addnqprlemrl  7389  addnqprlemru  7390  mulnqprlemrl  7405  mulnqprlemru  7406  ltpopr  7427  ltexprlemloc  7439  ltexprlemrl  7442  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  caucvgprlemladdfu  7509  suplocexprlemru  7551  axcaucvglemres  7731  cnegex  7964  mullt0  8266  eqord1  8269  mulge0  8405  divap0  8468  div2negap  8519  prodgt0  8634  ltmul12a  8642  recgt1i  8680  div4p1lem1div2  8997  nn0lt2  9156  peano5uzti  9183  btwnapz  9205  eluzp1m1  9373  eluzaddi  9376  eluzsubi  9377  uz2m1nn  9426  rphalflt  9500  xleaddadd  9700  ixxdisj  9716  iccgelb  9745  icodisj  9805  iccf1o  9817  fzsuc2  9890  fzonmapblen  9995  flqge0nn0  10097  flqge1nn  10098  modfzo0difsn  10199  expubnd  10381  bernneq  10443  bernneq2  10444  nn0opthlem2d  10499  facwordi  10518  bcpasc  10544  hashnncl  10574  recvguniq  10799  sqrt0rlem  10807  resqrexlemover  10814  resqrexlemcalc3  10820  resqrexlemgt0  10824  resqrexlemoverl  10825  recvalap  10901  nnabscl  10904  negfi  11031  climi0  11090  climge0  11126  summodclem3  11181  fsumsplit  11208  fisumcom2  11239  fisumrev2  11247  explecnv  11306  cvgratnnlemseq  11327  eftlub  11433  sin02gt0  11506  dvdslelemd  11577  dvdsleabs2  11580  mulmoddvds  11597  odd2np1  11606  oexpneg  11610  mod2eq1n2dvds  11612  sqoddm1div8z  11619  zsupcllemstep  11674  rplpwr  11751  rppwr  11752  nn0seqcvgd  11758  lcmneg  11791  qredeq  11813  dvdsnprmd  11842  oddprmge3  11851  oddpwdclemdvds  11884  oddpwdclemndvds  11885  oddpwdclemodd  11886  znege1  11892  qgt0numnn  11913  phibndlem  11928  hashgcdeq  11940  ennnfonelemf1  11967  neiuni  12369  neissex  12373  tgrest  12377  tgcnp  12417  lmfpm  12451  lmcl  12453  lmss  12454  lmff  12457  psmetdmdm  12532  xmeter  12644  neibl  12699  xmettxlem  12717  tgqioo  12755  cnopnap  12802  limcimo  12842  sinq12gt0  12959  logrpap0  13006  isomninnlem  13400  ismkvnnlem  13419