Theorem biimpa 296

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 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  simprbda  383  simplbda  384  pm5.1  603  biadanid  616  bimsc1  969  biimp3a  1379  equsex  1774  euor  2103  euan  2134  cgsexg  2835  cgsex2g  2836  cgsex4g  2837  ceqsex  2838  sbciegft  3059  sbeqalb  3085  sseqtrid  3274  exmidn0m  4285  euotd  4341  ralxfr2d  4555  rexxfr2d  4556  nlimsucg  4658  wetriext  4669  relop  4872  resiexg  5050  iotass  5296  fnbr  5425  f1o00  5608  foelcdmi  5686  fnex  5861  foelrn  5876  riotaeqimp  5979  acexmidlemab  5995  f1ocnv2d  6210  ofrval  6229  eloprabi  6342  1stconst  6367  2ndconst  6368  poxp  6378  smodm2  6441  smoiso  6448  nnsucuniel  6641  erth  6726  iinerm  6754  pw2f1odclem  6995  pw2f1odc  6996  phplem4dom  7023  findcard2  7051  findcard2s  7052  fimax2gtrilemstep  7062  undifdcss  7085  tpfidceq  7092  fipwssg  7146  supelti  7169  nlt1pig  7528  dfplpq2  7541  ltsonq  7585  archnqq  7604  nqnq0pi  7625  prarloclemn  7686  genprndl  7708  genprndu  7709  genpdisj  7710  addlocprlemgt  7721  addlocpr  7723  nqprl  7738  nqpru  7739  addnqprlemrl  7744  addnqprlemru  7745  mulnqprlemrl  7760  mulnqprlemru  7761  ltpopr  7782  ltexprlemloc  7794  ltexprlemrl  7797  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  caucvgprlemladdfu  7864  suplocexprlemru  7906  axcaucvglemres  8086  cnegex  8324  mullt0  8627  eqord1  8630  mulge0  8766  divap0  8831  div2negap  8882  prodgt0  8999  ltmul12a  9007  recgt1i  9045  div4p1lem1div2  9365  nn0lt2  9528  peano5uzti  9555  btwnapz  9577  eluzp1m1  9746  eluzaddi  9749  eluzsubi  9750  uz2m1nn  9800  rphalflt  9879  xleaddadd  10083  ixxdisj  10099  iccgelb  10128  icodisj  10188  iccf1o  10200  fzsuc2  10275  fzonmapblen  10387  zsupcllemstep  10449  nninfdcex  10457  flqge0nn0  10513  flqge1nn  10514  modfzo0difsn  10617  nninfinf  10665  seqf1oglem2  10742  expubnd  10818  bernneq  10882  bernneq2  10883  nn0opthlem2d  10943  facwordi  10962  bcpasc  10988  hashnncl  11017  ccatsymb  11137  ccatass  11143  ccat1st1st  11172  fzowrddc  11179  swrdlend  11190  swrdfv2  11195  swrdspsleq  11199  pfxeq  11228  pfxsuff1eqwrdeq  11231  swrdswrdlem  11236  swrdswrd  11237  swrdpfx  11239  ccats1pfxeqrex  11247  pfxccatin12lem1  11260  swrdccatin2  11261  recvguniq  11506  sqrt0rlem  11514  resqrexlemover  11521  resqrexlemcalc3  11527  resqrexlemgt0  11531  resqrexlemoverl  11532  recvalap  11608  nnabscl  11611  negfi  11739  2zinfmin  11754  climi0  11800  climge0  11836  summodclem3  11891  fsumsplit  11918  fisumcom2  11949  fisumrev2  11957  explecnv  12016  cvgratnnlemseq  12037  fprodsplitdc  12107  fprodsplit  12108  fprodcom2fi  12137  eftlub  12201  sin02gt0  12275  dvdslelemd  12354  dvdsleabs2  12357  mulmoddvds  12374  odd2np1  12384  oexpneg  12388  mod2eq1n2dvds  12390  sqoddm1div8z  12397  rplpwr  12548  rppwr  12549  nn0seqcvgd  12563  lcmneg  12596  qredeq  12618  dvdsnprmd  12647  oddprmge3  12657  oddpwdclemdvds  12692  oddpwdclemndvds  12693  oddpwdclemodd  12694  znege1  12700  qgt0numnn  12721  phibndlem  12738  hashgcdeq  12762  reumodprminv  12776  coprimeprodsq2  12781  pythagtrip  12806  pceq0  12845  dvdsprmpweqle  12860  fldivp1  12871  4sqlem9  12909  4sqlem15  12928  4sqlem16  12929  ennnfonelemf1  12989  imasmnd  13486  imasgrp  13648  subginv  13718  subgmulg  13725  eqger  13761  kerf1ghm  13811  rngpropd  13918  srgidmlem  13941  srg1zr  13950  ringpropd  14001  crngpropd  14002  imasring  14027  rhmf1o  14132  subrngpropd  14180  subrg1  14195  subrgpropd  14217  rrgnz  14232  aprsym  14248  aprcotr  14249  lmodprop2d  14312  lssssg  14324  lss0cl  14333  isridlrng  14446  rspcl  14455  rspssid  14456  rnglidlmmgm  14460  psrgrp  14649  mplsubgfilemcl  14663  neiuni  14835  neissex  14839  tgrest  14843  tgcnp  14883  lmfpm  14917  lmcl  14919  lmss  14920  lmff  14923  psmetdmdm  14998  xmeter  15110  neibl  15165  xmettxlem  15183  tgqioo  15229  cnopnap  15285  limcimo  15339  dvidsslem  15367  sinq12gt0  15504  logrpap0  15551  mersenne  15671  lgsdilem  15706  lgsdinn0  15727  gausslemma2dlem0b  15729  gausslemma2dlem1a  15737  gausslemma2dlem5  15745  gausslemma2dlem6  15746  lgsquad3  15763  m1lgs  15764  2lgslem1a  15767  2lgslem1  15770  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  2sqlem6  15799  edgupgren  15939  upgredg  15942  wlkl1loop  16069  wlk1walkdom  16070  upgriswlkdc  16071  2omap  16359  isomninnlem  16398  ismkvnnlem  16420