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  601  biadanid  614  bimsc1  965  biimp3a  1356  equsex  1742  euor  2071  euan  2101  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  ceqsex  2801  sbciegft  3020  sbeqalb  3046  sseqtrid  3234  exmidn0m  4235  euotd  4288  ralxfr2d  4500  rexxfr2d  4501  nlimsucg  4603  wetriext  4614  relop  4817  resiexg  4992  iotass  5237  fnbr  5363  f1o00  5542  foelcdmi  5616  fnex  5787  foelrn  5802  acexmidlemab  5919  f1ocnv2d  6131  ofrval  6150  eloprabi  6263  1stconst  6288  2ndconst  6289  poxp  6299  smodm2  6362  smoiso  6369  nnsucuniel  6562  erth  6647  iinerm  6675  pw2f1odclem  6904  pw2f1odc  6905  phplem4dom  6932  findcard2  6959  findcard2s  6960  fimax2gtrilemstep  6970  undifdcss  6993  tpfidceq  7000  fipwssg  7054  supelti  7077  nlt1pig  7427  dfplpq2  7440  ltsonq  7484  archnqq  7503  nqnq0pi  7524  prarloclemn  7585  genprndl  7607  genprndu  7608  genpdisj  7609  addlocprlemgt  7620  addlocpr  7622  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  mulnqprlemrl  7659  mulnqprlemru  7660  ltpopr  7681  ltexprlemloc  7693  ltexprlemrl  7696  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  caucvgprlemladdfu  7763  suplocexprlemru  7805  axcaucvglemres  7985  cnegex  8223  mullt0  8526  eqord1  8529  mulge0  8665  divap0  8730  div2negap  8781  prodgt0  8898  ltmul12a  8906  recgt1i  8944  div4p1lem1div2  9264  nn0lt2  9426  peano5uzti  9453  btwnapz  9475  eluzp1m1  9644  eluzaddi  9647  eluzsubi  9648  uz2m1nn  9698  rphalflt  9777  xleaddadd  9981  ixxdisj  9997  iccgelb  10026  icodisj  10086  iccf1o  10098  fzsuc2  10173  fzonmapblen  10282  zsupcllemstep  10338  nninfdcex  10346  flqge0nn0  10402  flqge1nn  10403  modfzo0difsn  10506  nninfinf  10554  seqf1oglem2  10631  expubnd  10707  bernneq  10771  bernneq2  10772  nn0opthlem2d  10832  facwordi  10851  bcpasc  10877  hashnncl  10906  recvguniq  11179  sqrt0rlem  11187  resqrexlemover  11194  resqrexlemcalc3  11200  resqrexlemgt0  11204  resqrexlemoverl  11205  recvalap  11281  nnabscl  11284  negfi  11412  2zinfmin  11427  climi0  11473  climge0  11509  summodclem3  11564  fsumsplit  11591  fisumcom2  11622  fisumrev2  11630  explecnv  11689  cvgratnnlemseq  11710  fprodsplitdc  11780  fprodsplit  11781  fprodcom2fi  11810  eftlub  11874  sin02gt0  11948  dvdslelemd  12027  dvdsleabs2  12030  mulmoddvds  12047  odd2np1  12057  oexpneg  12061  mod2eq1n2dvds  12063  sqoddm1div8z  12070  rplpwr  12221  rppwr  12222  nn0seqcvgd  12236  lcmneg  12269  qredeq  12291  dvdsnprmd  12320  oddprmge3  12330  oddpwdclemdvds  12365  oddpwdclemndvds  12366  oddpwdclemodd  12367  znege1  12373  qgt0numnn  12394  phibndlem  12411  hashgcdeq  12435  reumodprminv  12449  coprimeprodsq2  12454  pythagtrip  12479  pceq0  12518  dvdsprmpweqle  12533  fldivp1  12544  4sqlem9  12582  4sqlem15  12601  4sqlem16  12602  ennnfonelemf1  12662  imasmnd  13157  imasgrp  13319  subginv  13389  subgmulg  13396  eqger  13432  kerf1ghm  13482  rngpropd  13589  srgidmlem  13612  srg1zr  13621  ringpropd  13672  crngpropd  13673  imasring  13698  rhmf1o  13802  subrngpropd  13850  subrg1  13865  subrgpropd  13887  rrgnz  13902  aprsym  13918  aprcotr  13919  lmodprop2d  13982  lssssg  13994  lss0cl  14003  isridlrng  14116  rspcl  14125  rspssid  14126  rnglidlmmgm  14130  psrgrp  14319  mplsubgfilemcl  14333  neiuni  14505  neissex  14509  tgrest  14513  tgcnp  14553  lmfpm  14587  lmcl  14589  lmss  14590  lmff  14593  psmetdmdm  14668  xmeter  14780  neibl  14835  xmettxlem  14853  tgqioo  14899  cnopnap  14955  limcimo  15009  dvidsslem  15037  sinq12gt0  15174  logrpap0  15221  mersenne  15341  lgsdilem  15376  lgsdinn0  15397  gausslemma2dlem0b  15399  gausslemma2dlem1a  15407  gausslemma2dlem5  15415  gausslemma2dlem6  15416  lgsquad3  15433  m1lgs  15434  2lgslem1a  15437  2lgslem1  15440  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2sqlem6  15469  2omap  15750  isomninnlem  15787  ismkvnnlem  15809