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  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  4333  euotd  4390  ralxfr2d  4605  rexxfr2d  4606  nlimsucg  4708  wetriext  4719  relop  4925  resiexg  5103  iotass  5350  fnbr  5480  f1o00  5671  foelcdmi  5749  fnex  5928  foelrn  5948  riotaeqimp  6053  acexmidlemab  6069  f1ocnv2d  6284  f1o3d  6288  ofrval  6303  elabreximd  6346  eloprabi  6422  1stconst  6447  2ndconst  6448  poxp  6458  smodm2  6556  smoiso  6563  nnsucuniel  6758  erth  6843  iinerm  6871  pw2f1odclem  7124  pw2f1odc  7125  phplem4dom  7153  findcard2  7183  findcard2s  7184  fimax2gtrilemstep  7195  undifdcss  7220  tpfidceq  7227  fipwssg  7303  2omap  7308  supelti  7332  nlt1pig  7698  dfplpq2  7711  ltsonq  7755  archnqq  7774  nqnq0pi  7795  prarloclemn  7856  genprndl  7878  genprndu  7879  genpdisj  7880  addlocprlemgt  7891  addlocpr  7893  nqprl  7908  nqpru  7909  addnqprlemrl  7914  addnqprlemru  7915  mulnqprlemrl  7930  mulnqprlemru  7931  ltpopr  7952  ltexprlemloc  7964  ltexprlemrl  7967  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemladdfu  8034  suplocexprlemru  8076  axcaucvglemres  8256  cnegex  8494  mullt0  8798  eqord1  8801  mulge0  8937  divap0  9004  div2negap  9055  prodgt0  9172  ltmul12a  9180  recgt1i  9218  div4p1lem1div2  9538  nn0lt2  9706  peano5uzti  9733  btwnapz  9755  eluzp1m1  9925  eluzaddi  9928  eluzsubi  9929  uz2m1nn  9984  rphalflt  10063  xleaddadd  10268  ixxdisj  10284  iccgelb  10313  icodisj  10373  iccf1o  10386  fzsuc2  10464  fzonmapblen  10577  zsupcllemstep  10640  nninfdcex  10650  flqge0nn0  10706  flqge1nn  10707  modfzo0difsn  10810  nninfinf  10858  seqf1oglem2  10935  expubnd  11011  bernneq  11076  bernneq2  11077  nn0opthlem2d  11137  facwordi  11156  bcpasc  11182  hashnncl  11212  ccatsymb  11348  ccatass  11354  ccat1st1st  11387  fzowrddc  11397  swrdlend  11408  swrdfv2  11413  swrdspsleq  11417  pfxeq  11446  pfxsuff1eqwrdeq  11449  swrdswrdlem  11454  swrdswrd  11455  swrdpfx  11457  ccats1pfxeqrex  11465  pfxccatin12lem1  11478  swrdccatin2  11479  recvguniq  11739  sqrt0rlem  11747  resqrexlemover  11754  resqrexlemcalc3  11760  resqrexlemgt0  11764  resqrexlemoverl  11765  recvalap  11841  nnabscl  11844  negfi  11972  2zinfmin  11987  climi0  12033  climge0  12069  summodclem3  12125  fsumsplit  12152  fisumcom2  12183  fisumrev2  12191  explecnv  12250  cvgratnnlemseq  12271  fprodsplitdc  12341  fprodsplit  12342  fprodcom2fi  12371  eftlub  12435  sin02gt0  12509  dvdslelemd  12588  dvdsleabs2  12591  mulmoddvds  12608  odd2np1  12618  oexpneg  12622  mod2eq1n2dvds  12624  sqoddm1div8z  12631  rplpwr  12782  rppwr  12783  nn0seqcvgd  12797  lcmneg  12830  qredeq  12852  dvdsnprmd  12881  oddprmge3  12891  oddpwdclemdvds  12926  oddpwdclemndvds  12927  oddpwdclemodd  12928  znege1  12934  qgt0numnn  12955  phibndlem  12972  hashgcdeq  12996  reumodprminv  13010  coprimeprodsq2  13015  pythagtrip  13040  pceq0  13079  dvdsprmpweqle  13094  fldivp1  13105  4sqlem9  13143  4sqlem15  13162  4sqlem16  13163  ballotfilemfrcn0  13251  ennnfonelemf1  13287  imasmnd  13737  imasgrp  13891  subginv  13961  subgmulg  13968  eqger  14004  kerf1ghm  14054  rngpropd  14229  rng1zrlem  14233  srgidmlem  14256  ringpropd  14316  crngpropd  14317  imasring  14342  rhmf1o  14448  subrngpropd  14497  subrg1  14512  subrgpropd  14534  rrgnz  14550  aprsym  14569  aprcotr  14570  aprlring  14573  lmodprop2d  14657  lssssg  14669  lss0cl  14678  isridlrng  14791  rspcl  14800  rspssid  14801  rnglidlmmgm  14805  psrbagfsupp  14978  psrgrp  14999  mplsubgfilemcl  15013  neiuni  15185  neissex  15189  tgrest  15193  tgcnp  15233  lmfpm  15267  lmcl  15269  lmss  15270  lmff  15273  psmetdmdm  15348  xmeter  15460  neibl  15515  xmettxlem  15533  tgqioo  15579  cnopnap  15635  limcimo  15689  dvidsslem  15717  sinq12gt0  15854  logrpap0  15901  pellexlem2  16006  mersenne  16025  lgsdilem  16060  lgsdinn0  16081  gausslemma2dlem0b  16083  gausslemma2dlem1a  16091  gausslemma2dlem5  16099  gausslemma2dlem6  16100  lgsquad3  16117  m1lgs  16118  2lgslem1a  16121  2lgslem1  16124  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  2sqlem6  16153  edgupgren  16296  upgredg  16299  wlkl1loop  16513  wlk1walkdom  16514  upgriswlkdc  16515  loopclwwlkn1b  16574  eupth2lembfi  16632  dichmul0orlem6  16672  isomninnlem  16984  ismkvnnlem  17007