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  2835  cgsex2g  2836  cgsex4g  2837  ceqsex  2838  sbciegft  3059  sbeqalb  3085  sseqtrid  3274  exmidn0m  4285  euotd  4341  ralxfr2d  4555  rexxfr2d  4556  nlimsucg  4658  wetriext  4669  relop  4872  resiexg  5050  iotass  5296  fnbr  5425  f1o00  5610  foelcdmi  5688  fnex  5865  foelrn  5882  riotaeqimp  5985  acexmidlemab  6001  f1ocnv2d  6216  ofrval  6235  eloprabi  6348  1stconst  6373  2ndconst  6374  poxp  6384  smodm2  6447  smoiso  6454  nnsucuniel  6649  erth  6734  iinerm  6762  pw2f1odclem  7003  pw2f1odc  7004  phplem4dom  7031  findcard2  7059  findcard2s  7060  fimax2gtrilemstep  7071  undifdcss  7096  tpfidceq  7103  fipwssg  7157  supelti  7180  nlt1pig  7539  dfplpq2  7552  ltsonq  7596  archnqq  7615  nqnq0pi  7636  prarloclemn  7697  genprndl  7719  genprndu  7720  genpdisj  7721  addlocprlemgt  7732  addlocpr  7734  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  mulnqprlemrl  7771  mulnqprlemru  7772  ltpopr  7793  ltexprlemloc  7805  ltexprlemrl  7808  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemladdfu  7875  suplocexprlemru  7917  axcaucvglemres  8097  cnegex  8335  mullt0  8638  eqord1  8641  mulge0  8777  divap0  8842  div2negap  8893  prodgt0  9010  ltmul12a  9018  recgt1i  9056  div4p1lem1div2  9376  nn0lt2  9539  peano5uzti  9566  btwnapz  9588  eluzp1m1  9758  eluzaddi  9761  eluzsubi  9762  uz2m1nn  9812  rphalflt  9891  xleaddadd  10095  ixxdisj  10111  iccgelb  10140  icodisj  10200  iccf1o  10212  fzsuc2  10287  fzonmapblen  10399  zsupcllemstep  10461  nninfdcex  10469  flqge0nn0  10525  flqge1nn  10526  modfzo0difsn  10629  nninfinf  10677  seqf1oglem2  10754  expubnd  10830  bernneq  10894  bernneq2  10895  nn0opthlem2d  10955  facwordi  10974  bcpasc  11000  hashnncl  11029  ccatsymb  11150  ccatass  11156  ccat1st1st  11188  fzowrddc  11195  swrdlend  11206  swrdfv2  11211  swrdspsleq  11215  pfxeq  11244  pfxsuff1eqwrdeq  11247  swrdswrdlem  11252  swrdswrd  11253  swrdpfx  11255  ccats1pfxeqrex  11263  pfxccatin12lem1  11276  swrdccatin2  11277  recvguniq  11522  sqrt0rlem  11530  resqrexlemover  11537  resqrexlemcalc3  11543  resqrexlemgt0  11547  resqrexlemoverl  11548  recvalap  11624  nnabscl  11627  negfi  11755  2zinfmin  11770  climi0  11816  climge0  11852  summodclem3  11907  fsumsplit  11934  fisumcom2  11965  fisumrev2  11973  explecnv  12032  cvgratnnlemseq  12053  fprodsplitdc  12123  fprodsplit  12124  fprodcom2fi  12153  eftlub  12217  sin02gt0  12291  dvdslelemd  12370  dvdsleabs2  12373  mulmoddvds  12390  odd2np1  12400  oexpneg  12404  mod2eq1n2dvds  12406  sqoddm1div8z  12413  rplpwr  12564  rppwr  12565  nn0seqcvgd  12579  lcmneg  12612  qredeq  12634  dvdsnprmd  12663  oddprmge3  12673  oddpwdclemdvds  12708  oddpwdclemndvds  12709  oddpwdclemodd  12710  znege1  12716  qgt0numnn  12737  phibndlem  12754  hashgcdeq  12778  reumodprminv  12792  coprimeprodsq2  12797  pythagtrip  12822  pceq0  12861  dvdsprmpweqle  12876  fldivp1  12887  4sqlem9  12925  4sqlem15  12944  4sqlem16  12945  ennnfonelemf1  13005  imasmnd  13502  imasgrp  13664  subginv  13734  subgmulg  13741  eqger  13777  kerf1ghm  13827  rngpropd  13934  srgidmlem  13957  srg1zr  13966  ringpropd  14017  crngpropd  14018  imasring  14043  rhmf1o  14148  subrngpropd  14196  subrg1  14211  subrgpropd  14233  rrgnz  14248  aprsym  14264  aprcotr  14265  lmodprop2d  14328  lssssg  14340  lss0cl  14349  isridlrng  14462  rspcl  14471  rspssid  14472  rnglidlmmgm  14476  psrgrp  14665  mplsubgfilemcl  14679  neiuni  14851  neissex  14855  tgrest  14859  tgcnp  14899  lmfpm  14933  lmcl  14935  lmss  14936  lmff  14939  psmetdmdm  15014  xmeter  15126  neibl  15181  xmettxlem  15199  tgqioo  15245  cnopnap  15301  limcimo  15355  dvidsslem  15383  sinq12gt0  15520  logrpap0  15567  mersenne  15687  lgsdilem  15722  lgsdinn0  15743  gausslemma2dlem0b  15745  gausslemma2dlem1a  15753  gausslemma2dlem5  15761  gausslemma2dlem6  15762  lgsquad3  15779  m1lgs  15780  2lgslem1a  15783  2lgslem1  15786  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  2sqlem6  15815  edgupgren  15955  upgredg  15958  wlkl1loop  16104  wlk1walkdom  16105  upgriswlkdc  16106  loopclwwlkn1b  16161  2omap  16446  isomninnlem  16486  ismkvnnlem  16508