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 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117

This theorem is used by:  simprbda  383  simplbda  384  pm5.1  609  biadanid  622  bimsc1  976  biimp3a  1386  equsex  1780  euor  2112  euan  2143  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  ceqsex  2860  sbciegft  3082  sbeqalb  3108  sseqtrid  3298  exmidn0m  4338  euotd  4395  ralxfr2d  4610  rexxfr2d  4611  nlimsucg  4713  wetriext  4724  relop  4930  resiexg  5108  iotass  5355  fnbr  5485  f1o00  5676  foelcdmi  5755  fnex  5937  foelrn  5958  riotaeqimp  6063  acexmidlemab  6079  f1ocnv2d  6294  f1o3d  6298  ofrval  6313  elabreximd  6356  eloprabi  6432  1stconst  6457  2ndconst  6458  poxp  6468  smodm2  6566  smoiso  6573  nnsucuniel  6768  erth  6853  iinerm  6881  pw2f1odclem  7134  pw2f1odc  7135  phplem4dom  7163  findcard2  7193  findcard2s  7194  fimax2gtrilemstep  7205  undifdcss  7230  tpfidceq  7237  fipwssg  7313  2omap  7319  supelti  7343  nlt1pig  7709  dfplpq2  7722  ltsonq  7766  archnqq  7785  nqnq0pi  7806  prarloclemn  7867  genprndl  7889  genprndu  7890  genpdisj  7891  addlocprlemgt  7902  addlocpr  7904  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  mulnqprlemrl  7941  mulnqprlemru  7942  ltpopr  7963  ltexprlemloc  7975  ltexprlemrl  7978  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemladdfu  8045  suplocexprlemru  8087  axcaucvglemres  8267  cnegex  8506  mullt0  8810  eqord1  8813  mulge0  8950  divap0  9017  div2negap  9068  prodgt0  9185  ltmul12a  9193  recgt1i  9231  div4p1lem1div2  9564  nn0lt2  9732  peano5uzti  9759  btwnapz  9781  eluzp1m1  9956  eluzaddi  9959  eluzsubi  9960  uz2m1nn  10015  rphalflt  10095  xleaddadd  10300  ixxdisj  10316  iccgelb  10345  icodisj  10405  iccf1o  10418  fzsuc2  10497  fzonmapblen  10610  zsupcllemstep  10673  nninfdcex  10683  flqge0nn0  10743  flqge1nn  10744  modfzo0difsn  10847  nninfinf  10895  seqf1oglem2  10972  expubnd  11048  bernneq  11113  bernneq2  11114  nn0opthlem2d  11175  facwordi  11194  bcpasc  11220  hashnncl  11250  ccatsymb  11386  ccatass  11392  ccat1st1st  11425  fzowrddc  11435  swrdlend  11446  swrdfv2  11451  swrdspsleq  11455  pfxeq  11484  pfxsuff1eqwrdeq  11487  swrdswrdlem  11492  swrdswrd  11493  swrdpfx  11495  ccats1pfxeqrex  11503  pfxccatin12lem1  11516  swrdccatin2  11517  recvguniq  11777  sqrt0rlem  11785  resqrexlemover  11792  resqrexlemcalc3  11798  resqrexlemgt0  11802  resqrexlemoverl  11803  recvalap  11880  nnabscl  11883  negfi  12011  2zinfmin  12028  climi0  12074  climge0  12110  summodclem3  12166  fsumsplit  12193  fisumcom2  12224  fisumrev2  12232  explecnv  12291  cvgratnnlemseq  12312  fprodsplitdc  12382  fprodsplit  12383  fprodcom2fi  12412  eftlub  12476  sin02gt0  12550  dvdslelemd  12629  dvdsleabs2  12632  mulmoddvds  12649  odd2np1  12659  oexpneg  12663  mod2eq1n2dvds  12665  sqoddm1div8z  12672  rplpwr  12823  rppwr  12824  nn0seqcvgd  12838  lcmneg  12871  qredeq  12893  dvdsnprmd  12922  oddprmge3  12933  nnmaxpwlemdvds  12968  nnmaxpwlemndvds  12969  nnmaxpwlemnfac  12970  znege1  12977  qgt0numnn  12998  phibndlem  13017  hashgcdeq  13041  reumodprminv  13055  coprimeprodsq2  13060  pythagtrip  13085  pceq0  13124  dvdsprmpweqle  13139  fldivp1  13150  4sqlem9  13188  4sqlem15  13207  4sqlem16  13208  ballotfilemfrcn0  13325  ennnfonelemf1  13361  imasmnd  13813  imasgrp  13967  subginv  14037  subgmulg  14044  eqger  14080  kerf1ghm  14130  rngpropd  14338  rng1zrlem  14342  srgidmlem  14366  ringpropd  14427  crngpropd  14428  imasring  14453  rhmf1o  14559  subrngpropd  14608  subrg1  14623  subrgpropd  14645  rrgnz  14661  aprsym  14680  aprcotr  14681  aprlring  14684  lmodprop2d  14769  lssssg  14781  lss0cl  14790  isridlrng  14903  rspcl  14912  rspssid  14913  rnglidlmmgm  14917  psrbagfsupp  15139  psrbaglefifi  15147  psrgrp  15167  mplsubgfilemcl  15181  neiuni  15353  neissex  15357  tgrest  15361  tgcnp  15401  lmfpm  15435  lmcl  15437  lmss  15438  lmff  15441  psmetdmdm  15516  xmeter  15628  neibl  15683  xmettxlem  15701  tgqioo  15747  cnopnap  15803  limcimo  15857  dvidsslem  15885  sinq12gt0  16023  logrpap0  16071  pellexlem2  16191  ppiqeq0  16241  ppiqub  16254  chtqleppi  16255  mersenne  16258  lgsdilem  16312  lgsdinn0  16333  gausslemma2dlem0b  16335  gausslemma2dlem1a  16343  gausslemma2dlem5  16351  gausslemma2dlem6  16352  lgsquad3  16369  m1lgs  16370  2lgslem1a  16373  2lgslem1  16376  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  2sqlem6  16405  edgupgren  16548  upgredg  16551  wlkl1loop  16765  wlk1walkdom  16766  upgriswlkdc  16767  loopclwwlkn1b  16826  eupth2lembfi  16884  dichmul0orlem6  16924  isomninnlem  17245  ismkvnnlem  17269