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  2836  cgsex2g  2837  cgsex4g  2838  ceqsex  2839  sbciegft  3060  sbeqalb  3086  sseqtrid  3275  exmidn0m  4289  euotd  4345  ralxfr2d  4559  rexxfr2d  4560  nlimsucg  4662  wetriext  4673  relop  4878  resiexg  5056  iotass  5302  fnbr  5431  f1o00  5616  foelcdmi  5694  fnex  5871  foelrn  5888  riotaeqimp  5991  acexmidlemab  6007  f1ocnv2d  6222  ofrval  6241  eloprabi  6356  1stconst  6381  2ndconst  6382  poxp  6392  smodm2  6456  smoiso  6463  nnsucuniel  6658  erth  6743  iinerm  6771  pw2f1odclem  7015  pw2f1odc  7016  phplem4dom  7043  findcard2  7071  findcard2s  7072  fimax2gtrilemstep  7083  undifdcss  7108  tpfidceq  7115  fipwssg  7169  supelti  7192  nlt1pig  7551  dfplpq2  7564  ltsonq  7608  archnqq  7627  nqnq0pi  7648  prarloclemn  7709  genprndl  7731  genprndu  7732  genpdisj  7733  addlocprlemgt  7744  addlocpr  7746  nqprl  7761  nqpru  7762  addnqprlemrl  7767  addnqprlemru  7768  mulnqprlemrl  7783  mulnqprlemru  7784  ltpopr  7805  ltexprlemloc  7817  ltexprlemrl  7820  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  caucvgprlemladdfu  7887  suplocexprlemru  7929  axcaucvglemres  8109  cnegex  8347  mullt0  8650  eqord1  8653  mulge0  8789  divap0  8854  div2negap  8905  prodgt0  9022  ltmul12a  9030  recgt1i  9068  div4p1lem1div2  9388  nn0lt2  9551  peano5uzti  9578  btwnapz  9600  eluzp1m1  9770  eluzaddi  9773  eluzsubi  9774  uz2m1nn  9829  rphalflt  9908  xleaddadd  10112  ixxdisj  10128  iccgelb  10157  icodisj  10217  iccf1o  10229  fzsuc2  10304  fzonmapblen  10416  zsupcllemstep  10479  nninfdcex  10487  flqge0nn0  10543  flqge1nn  10544  modfzo0difsn  10647  nninfinf  10695  seqf1oglem2  10772  expubnd  10848  bernneq  10912  bernneq2  10913  nn0opthlem2d  10973  facwordi  10992  bcpasc  11018  hashnncl  11047  ccatsymb  11169  ccatass  11175  ccat1st1st  11208  fzowrddc  11218  swrdlend  11229  swrdfv2  11234  swrdspsleq  11238  pfxeq  11267  pfxsuff1eqwrdeq  11270  swrdswrdlem  11275  swrdswrd  11276  swrdpfx  11278  ccats1pfxeqrex  11286  pfxccatin12lem1  11299  swrdccatin2  11300  recvguniq  11546  sqrt0rlem  11554  resqrexlemover  11561  resqrexlemcalc3  11567  resqrexlemgt0  11571  resqrexlemoverl  11572  recvalap  11648  nnabscl  11651  negfi  11779  2zinfmin  11794  climi0  11840  climge0  11876  summodclem3  11931  fsumsplit  11958  fisumcom2  11989  fisumrev2  11997  explecnv  12056  cvgratnnlemseq  12077  fprodsplitdc  12147  fprodsplit  12148  fprodcom2fi  12177  eftlub  12241  sin02gt0  12315  dvdslelemd  12394  dvdsleabs2  12397  mulmoddvds  12414  odd2np1  12424  oexpneg  12428  mod2eq1n2dvds  12430  sqoddm1div8z  12437  rplpwr  12588  rppwr  12589  nn0seqcvgd  12603  lcmneg  12636  qredeq  12658  dvdsnprmd  12687  oddprmge3  12697  oddpwdclemdvds  12732  oddpwdclemndvds  12733  oddpwdclemodd  12734  znege1  12740  qgt0numnn  12761  phibndlem  12778  hashgcdeq  12802  reumodprminv  12816  coprimeprodsq2  12821  pythagtrip  12846  pceq0  12885  dvdsprmpweqle  12900  fldivp1  12911  4sqlem9  12949  4sqlem15  12968  4sqlem16  12969  ennnfonelemf1  13029  imasmnd  13526  imasgrp  13688  subginv  13758  subgmulg  13765  eqger  13801  kerf1ghm  13851  rngpropd  13958  srgidmlem  13981  srg1zr  13990  ringpropd  14041  crngpropd  14042  imasring  14067  rhmf1o  14172  subrngpropd  14220  subrg1  14235  subrgpropd  14257  rrgnz  14272  aprsym  14288  aprcotr  14289  lmodprop2d  14352  lssssg  14364  lss0cl  14373  isridlrng  14486  rspcl  14495  rspssid  14496  rnglidlmmgm  14500  psrgrp  14689  mplsubgfilemcl  14703  neiuni  14875  neissex  14879  tgrest  14883  tgcnp  14923  lmfpm  14957  lmcl  14959  lmss  14960  lmff  14963  psmetdmdm  15038  xmeter  15150  neibl  15205  xmettxlem  15223  tgqioo  15269  cnopnap  15325  limcimo  15379  dvidsslem  15407  sinq12gt0  15544  logrpap0  15591  mersenne  15711  lgsdilem  15746  lgsdinn0  15767  gausslemma2dlem0b  15769  gausslemma2dlem1a  15777  gausslemma2dlem5  15785  gausslemma2dlem6  15786  lgsquad3  15803  m1lgs  15804  2lgslem1a  15807  2lgslem1  15810  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  2sqlem6  15839  edgupgren  15980  upgredg  15983  wlkl1loop  16155  wlk1walkdom  16156  upgriswlkdc  16157  loopclwwlkn1b  16214  2omap  16530  isomninnlem  16570  ismkvnnlem  16592