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 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is referenced by:  biimp  118  simplbi  274  simprbda  383  simprld  530  simp1  999  eldifad  3155  unssad  3327  opth1  4254  opth  4255  0nelop  4266  epelg  4308  poirr  4325  brrelex1  4683  brrelex  4684  asymref  5032  soirri  5041  sotri  5042  fcnvres  5418  fun11iun  5501  elmpocl1  6092  f1od  6097  f1o2d  6099  oprssdmm  6196  smoiso  6327  tfrlem1  6333  swoer  6587  ecopovtrn  6658  ecopovtrng  6661  elmapssres  6699  pmresg  6702  mapsspm  6708  en1uniel  6830  pw2f1odc  6863  xpf1o  6872  sbthlemi9  6994  supelti  7031  supsnti  7034  supisoti  7039  ctssdccl  7140  ctfoex  7147  fodjum  7174  en2eleq  7224  djuen  7240  dftap2  7280  2omotaplemst  7287  exmidapne  7289  ccfunen  7293  dfplpq2  7383  ltbtwnnqq  7444  enq0tr  7463  elnp1st2nd  7505  prcdnql  7513  prnminu  7518  prloc  7520  genpcdl  7548  addnqprulem  7557  addlocprlemlt  7560  addlocprlemgt  7563  addlocprlem  7564  addlocpr  7565  nqprxx  7575  ltnqex  7578  addnqprlemfl  7588  addnqprlemfu  7589  appdivnq  7592  prmuloclemcalc  7594  prmuloc  7595  mullocprlem  7599  mulnqprlemfl  7604  mulnqprlemfu  7605  ltprordil  7618  ltnqpri  7623  ltexprlemm  7629  ltexprlemopl  7630  ltexprlemlol  7631  ltexprlemopu  7632  ltexprlemupu  7633  ltexprlemdisj  7635  ltexprlemloc  7636  ltexprlemfl  7638  ltexprlemrl  7639  ltexprlemfu  7640  ltexprlemru  7641  ltexpri  7642  lteupri  7646  ltaprlem  7647  recexprlemell  7651  recexprlemelu  7652  recexprlemloc  7660  recexprlempr  7661  recexprlem1ssl  7662  recexprlem1ssu  7663  recexprlemss1u  7665  aptipr  7670  cauappcvgprlemm  7674  cauappcvgprlemlol  7676  cauappcvgprlemladdfu  7683  cauappcvgprlemladdfl  7684  cauappcvgprlemladdru  7685  cauappcvgprlem1  7688  caucvgprlemnkj  7695  caucvgprlemnbj  7696  caucvgprlemm  7697  caucvgprlemlol  7699  caucvgprlemladdfu  7706  caucvgprprlemloccalc  7713  caucvgprprlemnkltj  7718  caucvgprprlemnbj  7722  caucvgprprlemml  7723  caucvgprprlemlol  7727  caucvgprprlemloc  7732  caucvgprprlemexbt  7735  suplocexprlemss  7744  suplocexprlemru  7748  suplocexprlemlub  7753  ltsrprg  7776  caucvgsrlemasr  7819  suplocsrlemb  7835  suplocsrlem  7837  suplocsr  7838  axcaucvglemcau  7927  axpre-suploclemres  7930  negf1o  8369  apreap  8574  apreim  8590  msqge0  8603  mulge0  8606  apti  8609  apsscn  8634  mulap0bad  8646  divadddivap  8714  recnz  9376  lbzbi  9646  xadd4d  9915  ixxss1  9934  ixxss2  9935  ixxss12  9936  iccss2  9974  iccssioo2  9976  iccssico2  9977  iccen  10036  elfzole1  10185  ioom  10291  elicore  10297  flqle  10309  flqltnz  10318  addmodlteq  10429  expclzap  10576  hashennnuni  10791  zfz1isolem1  10852  recl  10894  cvg1nlemcau  11025  cvg1nlemres  11026  resqrtth  11072  fimaxre2  11267  climcl  11322  reccn2ap  11353  nnf1o  11416  summodclem3  11420  sumpr  11453  fsump1i  11473  fisumcom2  11478  fsum00  11502  fsumparts  11510  mertenslemi1  11575  prodmodclem3  11615  fprodcom2fi  11666  addsin  11782  subsin  11783  addcos  11786  subcos  11787  sinbnd2  11794  cosbnd2  11795  sin01gt0  11801  cos01gt0  11802  divgcdz  12004  divgcdnn  12008  gcdaddm  12017  bezoutlemstep  12030  dvdsgcdb  12046  dfgcd2  12047  mulgcd  12049  gcdzeq  12055  dvdsmulgcd  12058  sqgcd  12062  bezoutr  12065  lcmval  12095  lcmcllem  12099  gcddvdslcm  12105  lcmgcdlem  12109  lcmgcd  12110  lcmgcdeq  12115  lcmdvdsb  12116  mulgcddvds  12126  rpmulgcd2  12127  qredeu  12129  rpdvds  12131  isprm3  12150  divgcdodd  12175  coprm  12176  rpexp  12185  sqrt2irr  12194  qnumcl  12220  qnumdencoprm  12225  divnumden  12228  numsq  12235  phimullem  12257  eulerthlem1  12259  prmdiveq  12268  prmdivdiv  12269  hashgcdlem  12270  odzcl  12275  reumodprminv  12285  pythagtriplem19  12314  pclemub  12319  pcprendvds  12322  pcprendvds2  12323  pcpre1  12324  pcpremul  12325  pceulem  12326  pceu  12327  pczpre  12329  pczcl  12330  pcgcd1  12360  pc2dvds  12362  pcaddlem  12371  pcmpt  12375  pockthlem  12388  prmunb  12394  4sqlem7  12416  4sqlem8  12417  4sqlem9  12418  4sqlem10  12419  4sqlem14  12436  4sqlem15  12437  4sqlem16  12438  4sqlem17  12439  4sqlem18  12440  ennnfonelemg  12454  ennnfonelemf1  12469  ctiunctlemu1st  12485  nninfdclemf  12500  nninfdclemp1  12501  mgmidcl  12854  mndlid  12896  dfgrp3mlem  13042  grplactf1o  13047  imasgrpf1  13054  subgsubm  13135  qusgrp  13171  ghmgrp1  13184  ghmf  13186  ghmnsgpreima  13208  kerf1ghm  13213  conjsubg  13216  imasrng  13310  srgdilem  13323  srgdi  13328  srglidm  13333  ringdilem  13366  ringdi  13372  ringlidm  13377  imasring  13414  imasringf1  13415  dvdsrcld  13447  unitcld  13458  unitmulcl  13463  unitnegcl  13480  rhmghm  13512  elrhmunit  13527  subrgss  13569  subrgrcl  13573  lmodvscl  13621  lmodvsdi  13627  lmodvsdir  13628  lsslsp  13745  qusring  13842  crngridl  13844  psrbaglesuppg  13950  psrelbas  13952  psraddcl  13956  uniopn  13961  restbasg  14128  cntop1  14161  cnf  14164  cnpf2  14167  lmtopcnp  14210  psmetdmdm  14284  psmetf  14285  psmet0  14287  xmetf  14310  metf  14311  blhalf  14368  xmetxpbl  14468  ioo2bl  14503  tgioo  14506  cncff  14524  rescncf  14528  cdivcncfap  14547  cnopnap  14554  dedekindeulemeu  14560  dedekindicclemeu  14569  ivthinclemlm  14572  ivthinclemlopn  14574  ivthinclemuopn  14576  ivthinclemdisj  14578  ivthdec  14582  limcimolemlt  14593  limcimo  14594  limccnpcntop  14604  limccnp2lem  14605  limccnp2cntop  14606  limccoap  14607  eldvap  14611  dvbsssg  14615  dvfgg  14617  dvaddxxbr  14625  dvmulxxbr  14626  dvcoapbr  14631  dvcj  14633  dvfre  14634  dvrecap  14637  sin0pilem1  14662  sin0pilem2  14663  pilem3  14664  tanrpcl  14718  tangtx  14719  lgsne0  14900  2sqlem8a  14930  2sqlem8  14931  nninfalllem1  15219  iooref1o  15244  alsi1d  15291  alsc1d  15293