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  972  biimp3a  1382  equsex  1776  euor  2105  euan  2136  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  ceqsex  2842  sbciegft  3063  sbeqalb  3089  sseqtrid  3278  exmidn0m  4297  euotd  4353  ralxfr2d  4567  rexxfr2d  4568  nlimsucg  4670  wetriext  4681  relop  4886  resiexg  5064  iotass  5311  fnbr  5441  f1o00  5629  foelcdmi  5707  fnex  5884  foelrn  5903  riotaeqimp  6006  acexmidlemab  6022  f1ocnv2d  6237  ofrval  6255  eloprabi  6370  1stconst  6395  2ndconst  6396  poxp  6406  smodm2  6504  smoiso  6511  nnsucuniel  6706  erth  6791  iinerm  6819  pw2f1odclem  7063  pw2f1odc  7064  phplem4dom  7091  findcard2  7121  findcard2s  7122  fimax2gtrilemstep  7133  undifdcss  7158  tpfidceq  7165  fipwssg  7238  supelti  7261  nlt1pig  7621  dfplpq2  7634  ltsonq  7678  archnqq  7697  nqnq0pi  7718  prarloclemn  7779  genprndl  7801  genprndu  7802  genpdisj  7803  addlocprlemgt  7814  addlocpr  7816  nqprl  7831  nqpru  7832  addnqprlemrl  7837  addnqprlemru  7838  mulnqprlemrl  7853  mulnqprlemru  7854  ltpopr  7875  ltexprlemloc  7887  ltexprlemrl  7890  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  caucvgprlemladdfu  7957  suplocexprlemru  7999  axcaucvglemres  8179  cnegex  8416  mullt0  8719  eqord1  8722  mulge0  8858  divap0  8923  div2negap  8974  prodgt0  9091  ltmul12a  9099  recgt1i  9137  div4p1lem1div2  9457  nn0lt2  9622  peano5uzti  9649  btwnapz  9671  eluzp1m1  9841  eluzaddi  9844  eluzsubi  9845  uz2m1nn  9900  rphalflt  9979  xleaddadd  10183  ixxdisj  10199  iccgelb  10228  icodisj  10288  iccf1o  10301  fzsuc2  10376  fzonmapblen  10489  zsupcllemstep  10552  nninfdcex  10560  flqge0nn0  10616  flqge1nn  10617  modfzo0difsn  10720  nninfinf  10768  seqf1oglem2  10845  expubnd  10921  bernneq  10985  bernneq2  10986  nn0opthlem2d  11046  facwordi  11065  bcpasc  11091  hashnncl  11120  ccatsymb  11245  ccatass  11251  ccat1st1st  11284  fzowrddc  11294  swrdlend  11305  swrdfv2  11310  swrdspsleq  11314  pfxeq  11343  pfxsuff1eqwrdeq  11346  swrdswrdlem  11351  swrdswrd  11352  swrdpfx  11354  ccats1pfxeqrex  11362  pfxccatin12lem1  11375  swrdccatin2  11376  recvguniq  11635  sqrt0rlem  11643  resqrexlemover  11650  resqrexlemcalc3  11656  resqrexlemgt0  11660  resqrexlemoverl  11661  recvalap  11737  nnabscl  11740  negfi  11868  2zinfmin  11883  climi0  11929  climge0  11965  summodclem3  12021  fsumsplit  12048  fisumcom2  12079  fisumrev2  12087  explecnv  12146  cvgratnnlemseq  12167  fprodsplitdc  12237  fprodsplit  12238  fprodcom2fi  12267  eftlub  12331  sin02gt0  12405  dvdslelemd  12484  dvdsleabs2  12487  mulmoddvds  12504  odd2np1  12514  oexpneg  12518  mod2eq1n2dvds  12520  sqoddm1div8z  12527  rplpwr  12678  rppwr  12679  nn0seqcvgd  12693  lcmneg  12726  qredeq  12748  dvdsnprmd  12777  oddprmge3  12787  oddpwdclemdvds  12822  oddpwdclemndvds  12823  oddpwdclemodd  12824  znege1  12830  qgt0numnn  12851  phibndlem  12868  hashgcdeq  12892  reumodprminv  12906  coprimeprodsq2  12911  pythagtrip  12936  pceq0  12975  dvdsprmpweqle  12990  fldivp1  13001  4sqlem9  13039  4sqlem15  13058  4sqlem16  13059  ennnfonelemf1  13119  imasmnd  13616  imasgrp  13778  subginv  13848  subgmulg  13855  eqger  13891  kerf1ghm  13941  rngpropd  14049  srgidmlem  14072  srg1zr  14081  ringpropd  14132  crngpropd  14133  imasring  14158  rhmf1o  14263  subrngpropd  14311  subrg1  14326  subrgpropd  14348  rrgnz  14364  aprsym  14380  aprcotr  14381  lmodprop2d  14444  lssssg  14456  lss0cl  14465  isridlrng  14578  rspcl  14587  rspssid  14588  rnglidlmmgm  14592  psrgrp  14786  mplsubgfilemcl  14800  neiuni  14972  neissex  14976  tgrest  14980  tgcnp  15020  lmfpm  15054  lmcl  15056  lmss  15057  lmff  15060  psmetdmdm  15135  xmeter  15247  neibl  15302  xmettxlem  15320  tgqioo  15366  cnopnap  15422  limcimo  15476  dvidsslem  15504  sinq12gt0  15641  logrpap0  15688  pellexlem2  15792  mersenne  15811  lgsdilem  15846  lgsdinn0  15867  gausslemma2dlem0b  15869  gausslemma2dlem1a  15877  gausslemma2dlem5  15885  gausslemma2dlem6  15886  lgsquad3  15903  m1lgs  15904  2lgslem1a  15907  2lgslem1  15910  2lgslem3a1  15916  2lgslem3b1  15917  2lgslem3c1  15918  2lgslem3d1  15919  2sqlem6  15939  edgupgren  16082  upgredg  16085  wlkl1loop  16299  wlk1walkdom  16300  upgriswlkdc  16301  loopclwwlkn1b  16360  eupth2lembfi  16418  2omap  16715  isomninnlem  16762  ismkvnnlem  16785