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  4286  euotd  4342  ralxfr2d  4556  rexxfr2d  4557  nlimsucg  4659  wetriext  4670  relop  4875  resiexg  5053  iotass  5299  fnbr  5428  f1o00  5613  foelcdmi  5691  fnex  5868  foelrn  5885  riotaeqimp  5988  acexmidlemab  6004  f1ocnv2d  6219  ofrval  6238  eloprabi  6353  1stconst  6378  2ndconst  6379  poxp  6389  smodm2  6452  smoiso  6459  nnsucuniel  6654  erth  6739  iinerm  6767  pw2f1odclem  7008  pw2f1odc  7009  phplem4dom  7036  findcard2  7064  findcard2s  7065  fimax2gtrilemstep  7076  undifdcss  7101  tpfidceq  7108  fipwssg  7162  supelti  7185  nlt1pig  7544  dfplpq2  7557  ltsonq  7601  archnqq  7620  nqnq0pi  7641  prarloclemn  7702  genprndl  7724  genprndu  7725  genpdisj  7726  addlocprlemgt  7737  addlocpr  7739  nqprl  7754  nqpru  7755  addnqprlemrl  7760  addnqprlemru  7761  mulnqprlemrl  7776  mulnqprlemru  7777  ltpopr  7798  ltexprlemloc  7810  ltexprlemrl  7813  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  caucvgprlemladdfu  7880  suplocexprlemru  7922  axcaucvglemres  8102  cnegex  8340  mullt0  8643  eqord1  8646  mulge0  8782  divap0  8847  div2negap  8898  prodgt0  9015  ltmul12a  9023  recgt1i  9061  div4p1lem1div2  9381  nn0lt2  9544  peano5uzti  9571  btwnapz  9593  eluzp1m1  9763  eluzaddi  9766  eluzsubi  9767  uz2m1nn  9817  rphalflt  9896  xleaddadd  10100  ixxdisj  10116  iccgelb  10145  icodisj  10205  iccf1o  10217  fzsuc2  10292  fzonmapblen  10404  zsupcllemstep  10466  nninfdcex  10474  flqge0nn0  10530  flqge1nn  10531  modfzo0difsn  10634  nninfinf  10682  seqf1oglem2  10759  expubnd  10835  bernneq  10899  bernneq2  10900  nn0opthlem2d  10960  facwordi  10979  bcpasc  11005  hashnncl  11034  ccatsymb  11155  ccatass  11161  ccat1st1st  11193  fzowrddc  11200  swrdlend  11211  swrdfv2  11216  swrdspsleq  11220  pfxeq  11249  pfxsuff1eqwrdeq  11252  swrdswrdlem  11257  swrdswrd  11258  swrdpfx  11260  ccats1pfxeqrex  11268  pfxccatin12lem1  11281  swrdccatin2  11282  recvguniq  11527  sqrt0rlem  11535  resqrexlemover  11542  resqrexlemcalc3  11548  resqrexlemgt0  11552  resqrexlemoverl  11553  recvalap  11629  nnabscl  11632  negfi  11760  2zinfmin  11775  climi0  11821  climge0  11857  summodclem3  11912  fsumsplit  11939  fisumcom2  11970  fisumrev2  11978  explecnv  12037  cvgratnnlemseq  12058  fprodsplitdc  12128  fprodsplit  12129  fprodcom2fi  12158  eftlub  12222  sin02gt0  12296  dvdslelemd  12375  dvdsleabs2  12378  mulmoddvds  12395  odd2np1  12405  oexpneg  12409  mod2eq1n2dvds  12411  sqoddm1div8z  12418  rplpwr  12569  rppwr  12570  nn0seqcvgd  12584  lcmneg  12617  qredeq  12639  dvdsnprmd  12668  oddprmge3  12678  oddpwdclemdvds  12713  oddpwdclemndvds  12714  oddpwdclemodd  12715  znege1  12721  qgt0numnn  12742  phibndlem  12759  hashgcdeq  12783  reumodprminv  12797  coprimeprodsq2  12802  pythagtrip  12827  pceq0  12866  dvdsprmpweqle  12881  fldivp1  12892  4sqlem9  12930  4sqlem15  12949  4sqlem16  12950  ennnfonelemf1  13010  imasmnd  13507  imasgrp  13669  subginv  13739  subgmulg  13746  eqger  13782  kerf1ghm  13832  rngpropd  13939  srgidmlem  13962  srg1zr  13971  ringpropd  14022  crngpropd  14023  imasring  14048  rhmf1o  14153  subrngpropd  14201  subrg1  14216  subrgpropd  14238  rrgnz  14253  aprsym  14269  aprcotr  14270  lmodprop2d  14333  lssssg  14345  lss0cl  14354  isridlrng  14467  rspcl  14476  rspssid  14477  rnglidlmmgm  14481  psrgrp  14670  mplsubgfilemcl  14684  neiuni  14856  neissex  14860  tgrest  14864  tgcnp  14904  lmfpm  14938  lmcl  14940  lmss  14941  lmff  14944  psmetdmdm  15019  xmeter  15131  neibl  15186  xmettxlem  15204  tgqioo  15250  cnopnap  15306  limcimo  15360  dvidsslem  15388  sinq12gt0  15525  logrpap0  15572  mersenne  15692  lgsdilem  15727  lgsdinn0  15748  gausslemma2dlem0b  15750  gausslemma2dlem1a  15758  gausslemma2dlem5  15766  gausslemma2dlem6  15767  lgsquad3  15784  m1lgs  15785  2lgslem1a  15788  2lgslem1  15791  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  2sqlem6  15820  edgupgren  15960  upgredg  15963  wlkl1loop  16130  wlk1walkdom  16131  upgriswlkdc  16132  loopclwwlkn1b  16187  2omap  16472  isomninnlem  16512  ismkvnnlem  16534