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  971  biimp3a  1381  equsex  1776  euor  2105  euan  2136  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  ceqsex  2841  sbciegft  3062  sbeqalb  3088  sseqtrid  3277  exmidn0m  4291  euotd  4347  ralxfr2d  4561  rexxfr2d  4562  nlimsucg  4664  wetriext  4675  relop  4880  resiexg  5058  iotass  5304  fnbr  5434  f1o00  5620  foelcdmi  5698  fnex  5876  foelrn  5893  riotaeqimp  5996  acexmidlemab  6012  f1ocnv2d  6227  ofrval  6246  eloprabi  6361  1stconst  6386  2ndconst  6387  poxp  6397  smodm2  6461  smoiso  6468  nnsucuniel  6663  erth  6748  iinerm  6776  pw2f1odclem  7020  pw2f1odc  7021  phplem4dom  7048  findcard2  7078  findcard2s  7079  fimax2gtrilemstep  7090  undifdcss  7115  tpfidceq  7122  fipwssg  7178  supelti  7201  nlt1pig  7561  dfplpq2  7574  ltsonq  7618  archnqq  7637  nqnq0pi  7658  prarloclemn  7719  genprndl  7741  genprndu  7742  genpdisj  7743  addlocprlemgt  7754  addlocpr  7756  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  mulnqprlemrl  7793  mulnqprlemru  7794  ltpopr  7815  ltexprlemloc  7827  ltexprlemrl  7830  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemladdfu  7897  suplocexprlemru  7939  axcaucvglemres  8119  cnegex  8357  mullt0  8660  eqord1  8663  mulge0  8799  divap0  8864  div2negap  8915  prodgt0  9032  ltmul12a  9040  recgt1i  9078  div4p1lem1div2  9398  nn0lt2  9561  peano5uzti  9588  btwnapz  9610  eluzp1m1  9780  eluzaddi  9783  eluzsubi  9784  uz2m1nn  9839  rphalflt  9918  xleaddadd  10122  ixxdisj  10138  iccgelb  10167  icodisj  10227  iccf1o  10239  fzsuc2  10314  fzonmapblen  10427  zsupcllemstep  10490  nninfdcex  10498  flqge0nn0  10554  flqge1nn  10555  modfzo0difsn  10658  nninfinf  10706  seqf1oglem2  10783  expubnd  10859  bernneq  10923  bernneq2  10924  nn0opthlem2d  10984  facwordi  11003  bcpasc  11029  hashnncl  11058  ccatsymb  11183  ccatass  11189  ccat1st1st  11222  fzowrddc  11232  swrdlend  11243  swrdfv2  11248  swrdspsleq  11252  pfxeq  11281  pfxsuff1eqwrdeq  11284  swrdswrdlem  11289  swrdswrd  11290  swrdpfx  11292  ccats1pfxeqrex  11300  pfxccatin12lem1  11313  swrdccatin2  11314  recvguniq  11573  sqrt0rlem  11581  resqrexlemover  11588  resqrexlemcalc3  11594  resqrexlemgt0  11598  resqrexlemoverl  11599  recvalap  11675  nnabscl  11678  negfi  11806  2zinfmin  11821  climi0  11867  climge0  11903  summodclem3  11959  fsumsplit  11986  fisumcom2  12017  fisumrev2  12025  explecnv  12084  cvgratnnlemseq  12105  fprodsplitdc  12175  fprodsplit  12176  fprodcom2fi  12205  eftlub  12269  sin02gt0  12343  dvdslelemd  12422  dvdsleabs2  12425  mulmoddvds  12442  odd2np1  12452  oexpneg  12456  mod2eq1n2dvds  12458  sqoddm1div8z  12465  rplpwr  12616  rppwr  12617  nn0seqcvgd  12631  lcmneg  12664  qredeq  12686  dvdsnprmd  12715  oddprmge3  12725  oddpwdclemdvds  12760  oddpwdclemndvds  12761  oddpwdclemodd  12762  znege1  12768  qgt0numnn  12789  phibndlem  12806  hashgcdeq  12830  reumodprminv  12844  coprimeprodsq2  12849  pythagtrip  12874  pceq0  12913  dvdsprmpweqle  12928  fldivp1  12939  4sqlem9  12977  4sqlem15  12996  4sqlem16  12997  ennnfonelemf1  13057  imasmnd  13554  imasgrp  13716  subginv  13786  subgmulg  13793  eqger  13829  kerf1ghm  13879  rngpropd  13987  srgidmlem  14010  srg1zr  14019  ringpropd  14070  crngpropd  14071  imasring  14096  rhmf1o  14201  subrngpropd  14249  subrg1  14264  subrgpropd  14286  rrgnz  14301  aprsym  14317  aprcotr  14318  lmodprop2d  14381  lssssg  14393  lss0cl  14402  isridlrng  14515  rspcl  14524  rspssid  14525  rnglidlmmgm  14529  psrgrp  14718  mplsubgfilemcl  14732  neiuni  14904  neissex  14908  tgrest  14912  tgcnp  14952  lmfpm  14986  lmcl  14988  lmss  14989  lmff  14992  psmetdmdm  15067  xmeter  15179  neibl  15234  xmettxlem  15252  tgqioo  15298  cnopnap  15354  limcimo  15408  dvidsslem  15436  sinq12gt0  15573  logrpap0  15620  mersenne  15740  lgsdilem  15775  lgsdinn0  15796  gausslemma2dlem0b  15798  gausslemma2dlem1a  15806  gausslemma2dlem5  15814  gausslemma2dlem6  15815  lgsquad3  15832  m1lgs  15833  2lgslem1a  15836  2lgslem1  15839  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  2sqlem6  15868  edgupgren  16011  upgredg  16014  wlkl1loop  16228  wlk1walkdom  16229  upgriswlkdc  16230  loopclwwlkn1b  16289  eupth2lembfi  16347  2omap  16645  isomninnlem  16685  ismkvnnlem  16708