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  4245  euotd  4299  ralxfr2d  4511  rexxfr2d  4512  nlimsucg  4614  wetriext  4625  relop  4828  resiexg  5004  iotass  5249  fnbr  5378  f1o00  5557  foelcdmi  5631  fnex  5806  foelrn  5821  acexmidlemab  5938  f1ocnv2d  6150  ofrval  6169  eloprabi  6282  1stconst  6307  2ndconst  6308  poxp  6318  smodm2  6381  smoiso  6388  nnsucuniel  6581  erth  6666  iinerm  6694  pw2f1odclem  6931  pw2f1odc  6932  phplem4dom  6959  findcard2  6986  findcard2s  6987  fimax2gtrilemstep  6997  undifdcss  7020  tpfidceq  7027  fipwssg  7081  supelti  7104  nlt1pig  7454  dfplpq2  7467  ltsonq  7511  archnqq  7530  nqnq0pi  7551  prarloclemn  7612  genprndl  7634  genprndu  7635  genpdisj  7636  addlocprlemgt  7647  addlocpr  7649  nqprl  7664  nqpru  7665  addnqprlemrl  7670  addnqprlemru  7671  mulnqprlemrl  7686  mulnqprlemru  7687  ltpopr  7708  ltexprlemloc  7720  ltexprlemrl  7723  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemladdfu  7790  suplocexprlemru  7832  axcaucvglemres  8012  cnegex  8250  mullt0  8553  eqord1  8556  mulge0  8692  divap0  8757  div2negap  8808  prodgt0  8925  ltmul12a  8933  recgt1i  8971  div4p1lem1div2  9291  nn0lt2  9454  peano5uzti  9481  btwnapz  9503  eluzp1m1  9672  eluzaddi  9675  eluzsubi  9676  uz2m1nn  9726  rphalflt  9805  xleaddadd  10009  ixxdisj  10025  iccgelb  10054  icodisj  10114  iccf1o  10126  fzsuc2  10201  fzonmapblen  10311  zsupcllemstep  10372  nninfdcex  10380  flqge0nn0  10436  flqge1nn  10437  modfzo0difsn  10540  nninfinf  10588  seqf1oglem2  10665  expubnd  10741  bernneq  10805  bernneq2  10806  nn0opthlem2d  10866  facwordi  10885  bcpasc  10911  hashnncl  10940  ccatsymb  11058  ccatass  11064  ccat1st1st  11093  fzowrddc  11100  swrdlend  11111  swrdfv2  11116  swrdspsleq  11120  recvguniq  11306  sqrt0rlem  11314  resqrexlemover  11321  resqrexlemcalc3  11327  resqrexlemgt0  11331  resqrexlemoverl  11332  recvalap  11408  nnabscl  11411  negfi  11539  2zinfmin  11554  climi0  11600  climge0  11636  summodclem3  11691  fsumsplit  11718  fisumcom2  11749  fisumrev2  11757  explecnv  11816  cvgratnnlemseq  11837  fprodsplitdc  11907  fprodsplit  11908  fprodcom2fi  11937  eftlub  12001  sin02gt0  12075  dvdslelemd  12154  dvdsleabs2  12157  mulmoddvds  12174  odd2np1  12184  oexpneg  12188  mod2eq1n2dvds  12190  sqoddm1div8z  12197  rplpwr  12348  rppwr  12349  nn0seqcvgd  12363  lcmneg  12396  qredeq  12418  dvdsnprmd  12447  oddprmge3  12457  oddpwdclemdvds  12492  oddpwdclemndvds  12493  oddpwdclemodd  12494  znege1  12500  qgt0numnn  12521  phibndlem  12538  hashgcdeq  12562  reumodprminv  12576  coprimeprodsq2  12581  pythagtrip  12606  pceq0  12645  dvdsprmpweqle  12660  fldivp1  12671  4sqlem9  12709  4sqlem15  12728  4sqlem16  12729  ennnfonelemf1  12789  imasmnd  13285  imasgrp  13447  subginv  13517  subgmulg  13524  eqger  13560  kerf1ghm  13610  rngpropd  13717  srgidmlem  13740  srg1zr  13749  ringpropd  13800  crngpropd  13801  imasring  13826  rhmf1o  13930  subrngpropd  13978  subrg1  13993  subrgpropd  14015  rrgnz  14030  aprsym  14046  aprcotr  14047  lmodprop2d  14110  lssssg  14122  lss0cl  14131  isridlrng  14244  rspcl  14253  rspssid  14254  rnglidlmmgm  14258  psrgrp  14447  mplsubgfilemcl  14461  neiuni  14633  neissex  14637  tgrest  14641  tgcnp  14681  lmfpm  14715  lmcl  14717  lmss  14718  lmff  14721  psmetdmdm  14796  xmeter  14908  neibl  14963  xmettxlem  14981  tgqioo  15027  cnopnap  15083  limcimo  15137  dvidsslem  15165  sinq12gt0  15302  logrpap0  15349  mersenne  15469  lgsdilem  15504  lgsdinn0  15525  gausslemma2dlem0b  15527  gausslemma2dlem1a  15535  gausslemma2dlem5  15543  gausslemma2dlem6  15544  lgsquad3  15561  m1lgs  15562  2lgslem1a  15565  2lgslem1  15568  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  2sqlem6  15597  2omap  15932  isomninnlem  15969  ismkvnnlem  15991