Theorem simpld 112

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
simpld.1	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simpld	⊢ (𝜑 → 𝜓)

Proof of Theorem simpld

Step	Hyp	Ref	Expression
1		simpld.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is used by:  biimp  118  simplbi  274  simprbda  383  simplld  532  simplrd  534  simprld  536  simp1  1028  eldifad  3231  unssad  3406  opth1  4376  opth  4377  0nelop  4388  epelg  4435  poirr  4452  brrelex1  4814  brrelex  4815  asymref  5173  soirri  5182  sotri  5183  ffdmd  5559  fcnvres  5575  fun11iun  5660  funopsn  5891  elmpocl1  6285  f1od  6293  f1o2d  6295  oprssdmm  6405  elmpom  6474  fczsupp0  6499  smoiso  6573  tfrlem1  6579  swoer  6835  ecopovtrn  6906  ecopovtrng  6909  elmapssres  6954  pmresg  6957  mapsspm  6963  en1uniel  7091  pw2f1odc  7135  xpf1o  7144  sbthlemi9  7282  fsuppfund  7294  supelti  7342  supsnti  7345  supisoti  7350  ctssdccl  7451  ctfoex  7458  fodjum  7486  en2eleq  7547  djuen  7567  pw1if  7584  dftap2  7617  2omotaplemst  7624  exmidapne  7626  ccfunen  7630  dfplpq2  7721  ltbtwnnqq  7782  enq0tr  7801  elnp1st2nd  7843  prcdnql  7851  prnminu  7856  prloc  7858  genpcdl  7886  addnqprulem  7895  addlocprlemlt  7898  addlocprlemgt  7901  addlocprlem  7902  addlocpr  7903  nqprxx  7913  ltnqex  7916  addnqprlemfl  7926  addnqprlemfu  7927  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mullocprlem  7937  mulnqprlemfl  7942  mulnqprlemfu  7943  ltprordil  7956  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltexpri  7980  lteupri  7984  ltaprlem  7985  recexprlemell  7989  recexprlemelu  7990  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1u  8003  aptipr  8008  cauappcvgprlemm  8012  cauappcvgprlemlol  8014  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlem1  8026  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemlol  8037  caucvgprlemladdfu  8044  caucvgprprlemloccalc  8051  caucvgprprlemnkltj  8056  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemlol  8065  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  suplocexprlemss  8082  suplocexprlemru  8086  suplocexprlemlub  8091  ltsrprg  8114  caucvgsrlemasr  8157  suplocsrlemb  8173  suplocsrlem  8175  suplocsr  8176  axcaucvglemcau  8265  axpre-suploclemres  8268  negf1o  8709  apreap  8916  apreim  8932  msqge0  8945  mulge0  8948  apti  8951  apsscn  8976  mulap0bad  8988  divadddivap  9058  recnz  9741  lbzbi  10018  xadd4d  10289  ixxss1  10308  ixxss2  10309  ixxss12  10310  iccss2  10348  iccssioo2  10350  iccssico2  10351  iccen  10411  elfzole1  10565  infssfzcldc  10671  infssfzledc  10672  ioom  10697  elicore  10703  flqle  10715  flqltnz  10724  addmodlteq  10837  expclzap  11003  hashennnuni  11220  zfz1isolem1  11294  hashdmprop2dom  11298  swrdsbslen  11440  ccatswrd  11444  ccatpfx  11475  recl  11620  sq01  11662  cvg1nlemcau  11752  cvg1nlemres  11753  resqrtth  11799  fimaxre2  11995  climcl  12050  reccn2ap  12081  nnf1o  12145  summodclem3  12149  sumpr  12182  fsump1i  12202  fisumcom2  12207  fsum00  12231  fsumparts  12239  mertenslemi1  12304  prodmodclem3  12344  fprodcom2fi  12395  addsin  12511  subsin  12512  addcos  12515  subcos  12516  sinbnd2  12523  cosbnd2  12524  sin01gt0  12531  cos01gt0  12532  divgcdz  12750  divgcdnn  12754  gcdaddm  12763  bezoutlemstep  12776  dvdsgcdb  12792  dfgcd2  12793  mulgcd  12795  gcdzeq  12801  dvdsmulgcd  12804  sqgcd  12808  bezoutr  12811  lcmval  12843  lcmcllem  12847  gcddvdslcm  12853  lcmgcdlem  12857  lcmgcd  12858  lcmgcdeq  12863  lcmdvdsb  12864  mulgcddvds  12874  rpmulgcd2  12875  qredeu  12877  rpdvds  12879  isprm3  12898  divgcdodd  12923  coprm  12924  rpexp  12933  sqrt2irr  12942  qnumcl  12968  qnumdencoprm  12973  divnumden  12976  numsq  12983  phimullem  13005  eulerthlem1  13007  prmdiveq  13016  prmdivdiv  13017  hashgcdlem  13018  odzcl  13024  reumodprminv  13034  pythagtriplem19  13063  pclemub  13068  pcprendvds  13071  pcprendvds2  13072  pcpre1  13073  pcpremul  13074  pceulem  13075  pceu  13076  pczpre  13078  pczcl  13079  pcgcd1  13109  pc2dvds  13111  pcaddlem  13120  pcmpt  13124  pockthlem  13137  prmunb  13143  4sqlem7  13165  4sqlem8  13166  4sqlem9  13167  4sqlem10  13168  4sqlem14  13185  4sqlem15  13186  4sqlem16  13187  4sqlem17  13188  4sqlem18  13189  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilem4  13243  ballotfilemi1  13247  ballotfilemimin  13251  ballotfilemic  13252  ballotfilem1c  13253  ballotfilemsv  13255  ballotfilemsgt1  13256  ballotfilemsdom  13257  ballotfilemsel1i  13258  ballotfilemsf1o  13259  ballotfilemsi  13260  ballotfilemsima  13261  ballotfilemscr  13264  ballotfilemrv  13265  ballotfilemrv2  13267  ballotfilemro  13268  ballotfilemfrc  13272  ballotfilemfrci  13273  ballotfilemfrceq  13274  ballotfilemfrcn0  13275  ballotfilemrc  13276  ballotfilemirc  13277  ballotfilemrinv0  13278  ballotfilem1ri  13280  ennnfonelemg  13296  ennnfonelemf1  13311  ctiunctlemu1st  13327  nninfdclemf  13342  nninfdclemp1  13343  mgmidcl  13700  gzsumfzval  13713  gzsumval2  13716  mndlid  13750  imasmndf1  13763  dfgrp3mlem  13905  grplactf1o  13910  imasgrpf1  13917  subgsubm  14001  qusgrp  14037  ghmgrp1  14050  ghmf  14052  ghmnsgpreima  14074  kerf1ghm  14079  conjsubg  14082  gzsumsplit0  14150  gsumvalfi  14154  prdsmndd  14196  prdsgrpd  14199  prdsinvgd  14200  imasrng  14257  srgdilem  14275  srgdi  14280  srglidm  14285  ringdilem  14318  ringdi  14325  ringlidm  14330  imasring  14371  imasringf1  14372  dvdsrcld  14406  unitcld  14417  unitmulcl  14422  unitnegcl  14439  rhmghm  14471  elrhmunit  14486  subrgss  14532  subrgrcl  14536  rrgsupp  14576  lmodvscl  14643  lmodvsdi  14650  lmodvsdir  14651  lsslsp  14768  qusring  14866  crngridl  14869  znunit  14996  znrrg  14997  assaass  15006  assalmod  15008  psrbaglesuppg  15059  psrbagcon  15064  psrbagconcl  15065  psrelbas  15068  psraddcl  15073  mplrcl  15087  uniopn  15104  restbasg  15271  cntop1  15304  cnf  15307  cnpf2  15310  lmtopcnp  15353  psmetdmdm  15427  psmetf  15428  psmet0  15430  xmetf  15453  metf  15454  blhalf  15511  xmetxpbl  15611  ioo2bl  15654  tgioo  15657  cncff  15680  rescncf  15684  cdivcncfap  15707  cnopnap  15714  divcncfap  15717  dedekindeulemeu  15725  dedekindicclemeu  15734  ivthinclemlm  15737  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthinclemdisj  15743  ivthdec  15747  ivthreinc  15748  limcimolemlt  15767  limcimo  15768  limccnpcntop  15778  limccnp2lem  15779  limccnp2cntop  15780  limccoap  15781  eldvap  15785  dvbsssg  15789  dvfgg  15791  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvcj  15812  dvfre  15813  dvrecap  15816  plyco  15862  plycj  15864  sin0pilem1  15885  sin0pilem2  15886  pilem3  15887  tanrpcl  15941  tangtx  15942  perfect  16121  lgsne0  16169  lgseisen  16205  lgsquad2lem2  16213  2sqlem8a  16253  2sqlem8  16254  structgrssvtx  16295  edguhgr  16390  umgrpredgv  16400  umgrnloop2  16404  umgr2edg  16460  subuhgr  16525  subumgr  16527  subusgr  16528  wlkpropg  16577  wlkv  16579  wlkvtxeledgg  16597  wlkvtxiedgg  16599  wlk1walkdom  16612  trlsv  16637  clwwlksswrd  16650  clwwlkclwwlkn  16662  eupthv  16699  eupthseg  16705  eupth2lem3lem3fi  16723  eupth2lem3lem4fi  16726  eupth2lemsfi  16731  eulerpathprum  16733  nninfalllem1  17063  iooref1o  17095  als1d  17145  rals1d  17147  alseu1d  17181  ralseu1d  17183