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  601  biadanid  614  bimsc1  966  biimp3a  1358  equsex  1751  euor  2080  euan  2110  cgsexg  2807  cgsex2g  2808  cgsex4g  2809  ceqsex  2810  sbciegft  3029  sbeqalb  3055  sseqtrid  3243  exmidn0m  4246  euotd  4300  ralxfr2d  4512  rexxfr2d  4513  nlimsucg  4615  wetriext  4626  relop  4829  resiexg  5005  iotass  5250  fnbr  5379  f1o00  5559  foelcdmi  5633  fnex  5808  foelrn  5823  acexmidlemab  5940  f1ocnv2d  6152  ofrval  6171  eloprabi  6284  1stconst  6309  2ndconst  6310  poxp  6320  smodm2  6383  smoiso  6390  nnsucuniel  6583  erth  6668  iinerm  6696  pw2f1odclem  6933  pw2f1odc  6934  phplem4dom  6961  findcard2  6988  findcard2s  6989  fimax2gtrilemstep  6999  undifdcss  7022  tpfidceq  7029  fipwssg  7083  supelti  7106  nlt1pig  7456  dfplpq2  7469  ltsonq  7513  archnqq  7532  nqnq0pi  7553  prarloclemn  7614  genprndl  7636  genprndu  7637  genpdisj  7638  addlocprlemgt  7649  addlocpr  7651  nqprl  7666  nqpru  7667  addnqprlemrl  7672  addnqprlemru  7673  mulnqprlemrl  7688  mulnqprlemru  7689  ltpopr  7710  ltexprlemloc  7722  ltexprlemrl  7725  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  caucvgprlemladdfu  7792  suplocexprlemru  7834  axcaucvglemres  8014  cnegex  8252  mullt0  8555  eqord1  8558  mulge0  8694  divap0  8759  div2negap  8810  prodgt0  8927  ltmul12a  8935  recgt1i  8973  div4p1lem1div2  9293  nn0lt2  9456  peano5uzti  9483  btwnapz  9505  eluzp1m1  9674  eluzaddi  9677  eluzsubi  9678  uz2m1nn  9728  rphalflt  9807  xleaddadd  10011  ixxdisj  10027  iccgelb  10056  icodisj  10116  iccf1o  10128  fzsuc2  10203  fzonmapblen  10313  zsupcllemstep  10374  nninfdcex  10382  flqge0nn0  10438  flqge1nn  10439  modfzo0difsn  10542  nninfinf  10590  seqf1oglem2  10667  expubnd  10743  bernneq  10807  bernneq2  10808  nn0opthlem2d  10868  facwordi  10887  bcpasc  10913  hashnncl  10942  ccatsymb  11061  ccatass  11067  ccat1st1st  11096  fzowrddc  11103  swrdlend  11114  swrdfv2  11119  swrdspsleq  11123  pfxeq  11150  pfxsuff1eqwrdeq  11153  recvguniq  11339  sqrt0rlem  11347  resqrexlemover  11354  resqrexlemcalc3  11360  resqrexlemgt0  11364  resqrexlemoverl  11365  recvalap  11441  nnabscl  11444  negfi  11572  2zinfmin  11587  climi0  11633  climge0  11669  summodclem3  11724  fsumsplit  11751  fisumcom2  11782  fisumrev2  11790  explecnv  11849  cvgratnnlemseq  11870  fprodsplitdc  11940  fprodsplit  11941  fprodcom2fi  11970  eftlub  12034  sin02gt0  12108  dvdslelemd  12187  dvdsleabs2  12190  mulmoddvds  12207  odd2np1  12217  oexpneg  12221  mod2eq1n2dvds  12223  sqoddm1div8z  12230  rplpwr  12381  rppwr  12382  nn0seqcvgd  12396  lcmneg  12429  qredeq  12451  dvdsnprmd  12480  oddprmge3  12490  oddpwdclemdvds  12525  oddpwdclemndvds  12526  oddpwdclemodd  12527  znege1  12533  qgt0numnn  12554  phibndlem  12571  hashgcdeq  12595  reumodprminv  12609  coprimeprodsq2  12614  pythagtrip  12639  pceq0  12678  dvdsprmpweqle  12693  fldivp1  12704  4sqlem9  12742  4sqlem15  12761  4sqlem16  12762  ennnfonelemf1  12822  imasmnd  13318  imasgrp  13480  subginv  13550  subgmulg  13557  eqger  13593  kerf1ghm  13643  rngpropd  13750  srgidmlem  13773  srg1zr  13782  ringpropd  13833  crngpropd  13834  imasring  13859  rhmf1o  13963  subrngpropd  14011  subrg1  14026  subrgpropd  14048  rrgnz  14063  aprsym  14079  aprcotr  14080  lmodprop2d  14143  lssssg  14155  lss0cl  14164  isridlrng  14277  rspcl  14286  rspssid  14287  rnglidlmmgm  14291  psrgrp  14480  mplsubgfilemcl  14494  neiuni  14666  neissex  14670  tgrest  14674  tgcnp  14714  lmfpm  14748  lmcl  14750  lmss  14751  lmff  14754  psmetdmdm  14829  xmeter  14941  neibl  14996  xmettxlem  15014  tgqioo  15060  cnopnap  15116  limcimo  15170  dvidsslem  15198  sinq12gt0  15335  logrpap0  15382  mersenne  15502  lgsdilem  15537  lgsdinn0  15558  gausslemma2dlem0b  15560  gausslemma2dlem1a  15568  gausslemma2dlem5  15576  gausslemma2dlem6  15577  lgsquad3  15594  m1lgs  15595  2lgslem1a  15598  2lgslem1  15601  2lgslem3a1  15607  2lgslem3b1  15608  2lgslem3c1  15609  2lgslem3d1  15610  2sqlem6  15630  2omap  15969  isomninnlem  16006  ismkvnnlem  16028