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  605  biadanid  618  bimsc1  972  biimp3a  1382  equsex  1776  euor  2108  euan  2139  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  ceqsex  2854  sbciegft  3075  sbeqalb  3101  sseqtrid  3290  exmidn0m  4316  euotd  4373  ralxfr2d  4587  rexxfr2d  4588  nlimsucg  4690  wetriext  4701  relop  4907  resiexg  5085  iotass  5332  fnbr  5462  f1o00  5653  foelcdmi  5731  fnex  5908  foelrn  5927  riotaeqimp  6030  acexmidlemab  6046  f1ocnv2d  6261  ofrval  6279  eloprabi  6394  1stconst  6419  2ndconst  6420  poxp  6430  smodm2  6528  smoiso  6535  nnsucuniel  6730  erth  6815  iinerm  6843  pw2f1odclem  7089  pw2f1odc  7090  phplem4dom  7118  findcard2  7148  findcard2s  7149  fimax2gtrilemstep  7160  undifdcss  7185  tpfidceq  7192  fipwssg  7268  2omap  7271  supelti  7295  nlt1pig  7658  dfplpq2  7671  ltsonq  7715  archnqq  7734  nqnq0pi  7755  prarloclemn  7816  genprndl  7838  genprndu  7839  genpdisj  7840  addlocprlemgt  7851  addlocpr  7853  nqprl  7868  nqpru  7869  addnqprlemrl  7874  addnqprlemru  7875  mulnqprlemrl  7890  mulnqprlemru  7891  ltpopr  7912  ltexprlemloc  7924  ltexprlemrl  7927  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  caucvgprlemladdfu  7994  suplocexprlemru  8036  axcaucvglemres  8216  cnegex  8453  mullt0  8756  eqord1  8759  mulge0  8895  divap0  8960  div2negap  9011  prodgt0  9128  ltmul12a  9136  recgt1i  9174  div4p1lem1div2  9494  nn0lt2  9662  peano5uzti  9689  btwnapz  9711  eluzp1m1  9881  eluzaddi  9884  eluzsubi  9885  uz2m1nn  9940  rphalflt  10019  xleaddadd  10223  ixxdisj  10239  iccgelb  10268  icodisj  10328  iccf1o  10341  fzsuc2  10417  fzonmapblen  10530  zsupcllemstep  10593  nninfdcex  10601  flqge0nn0  10657  flqge1nn  10658  modfzo0difsn  10761  nninfinf  10809  seqf1oglem2  10886  expubnd  10962  bernneq  11026  bernneq2  11027  nn0opthlem2d  11087  facwordi  11106  bcpasc  11132  hashnncl  11162  ccatsymb  11294  ccatass  11300  ccat1st1st  11333  fzowrddc  11343  swrdlend  11354  swrdfv2  11359  swrdspsleq  11363  pfxeq  11392  pfxsuff1eqwrdeq  11395  swrdswrdlem  11400  swrdswrd  11401  swrdpfx  11403  ccats1pfxeqrex  11411  pfxccatin12lem1  11424  swrdccatin2  11425  recvguniq  11684  sqrt0rlem  11692  resqrexlemover  11699  resqrexlemcalc3  11705  resqrexlemgt0  11709  resqrexlemoverl  11710  recvalap  11786  nnabscl  11789  negfi  11917  2zinfmin  11932  climi0  11978  climge0  12014  summodclem3  12070  fsumsplit  12097  fisumcom2  12128  fisumrev2  12136  explecnv  12195  cvgratnnlemseq  12216  fprodsplitdc  12286  fprodsplit  12287  fprodcom2fi  12316  eftlub  12380  sin02gt0  12454  dvdslelemd  12533  dvdsleabs2  12536  mulmoddvds  12553  odd2np1  12563  oexpneg  12567  mod2eq1n2dvds  12569  sqoddm1div8z  12576  rplpwr  12727  rppwr  12728  nn0seqcvgd  12742  lcmneg  12775  qredeq  12797  dvdsnprmd  12826  oddprmge3  12836  oddpwdclemdvds  12871  oddpwdclemndvds  12872  oddpwdclemodd  12873  znege1  12879  qgt0numnn  12900  phibndlem  12917  hashgcdeq  12941  reumodprminv  12955  coprimeprodsq2  12960  pythagtrip  12985  pceq0  13024  dvdsprmpweqle  13039  fldivp1  13050  4sqlem9  13088  4sqlem15  13107  4sqlem16  13108  ennnfonelemf1  13186  imasmnd  13683  imasgrp  13845  subginv  13915  subgmulg  13922  eqger  13958  kerf1ghm  14008  rngpropd  14116  srgidmlem  14139  srg1zr  14148  ringpropd  14199  crngpropd  14200  imasring  14225  rhmf1o  14330  subrngpropd  14378  subrg1  14393  subrgpropd  14415  rrgnz  14431  aprsym  14447  aprcotr  14448  aprlring  14451  lmodprop2d  14513  lssssg  14525  lss0cl  14534  isridlrng  14647  rspcl  14656  rspssid  14657  rnglidlmmgm  14661  psrbagfsupp  14836  psrgrp  14857  mplsubgfilemcl  14871  neiuni  15043  neissex  15047  tgrest  15051  tgcnp  15091  lmfpm  15125  lmcl  15127  lmss  15128  lmff  15131  psmetdmdm  15206  xmeter  15318  neibl  15373  xmettxlem  15391  tgqioo  15437  cnopnap  15493  limcimo  15547  dvidsslem  15575  sinq12gt0  15712  logrpap0  15759  pellexlem2  15863  mersenne  15882  lgsdilem  15917  lgsdinn0  15938  gausslemma2dlem0b  15940  gausslemma2dlem1a  15948  gausslemma2dlem5  15956  gausslemma2dlem6  15957  lgsquad3  15974  m1lgs  15975  2lgslem1a  15978  2lgslem1  15981  2lgslem3a1  15987  2lgslem3b1  15988  2lgslem3c1  15989  2lgslem3d1  15990  2sqlem6  16010  edgupgren  16153  upgredg  16156  wlkl1loop  16370  wlk1walkdom  16371  upgriswlkdc  16372  loopclwwlkn1b  16431  eupth2lembfi  16489  isomninnlem  16831  ismkvnnlem  16854