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  1021  eldifad  3209  unssad  3382  opth1  4326  opth  4327  0nelop  4338  epelg  4385  poirr  4402  brrelex1  4763  brrelex  4764  asymref  5120  soirri  5129  sotri  5130  ffdmd  5503  fcnvres  5517  fun11iun  5601  funopsn  5825  elmpocl1  6213  f1od  6221  f1o2d  6223  oprssdmm  6329  elmpom  6398  smoiso  6463  tfrlem1  6469  swoer  6725  ecopovtrn  6796  ecopovtrng  6799  elmapssres  6837  pmresg  6840  mapsspm  6846  en1uniel  6973  pw2f1odc  7016  xpf1o  7025  sbthlemi9  7158  supelti  7195  supsnti  7198  supisoti  7203  ctssdccl  7304  ctfoex  7311  fodjum  7339  en2eleq  7399  djuen  7419  pw1if  7436  dftap2  7463  2omotaplemst  7470  exmidapne  7472  ccfunen  7476  dfplpq2  7567  ltbtwnnqq  7628  enq0tr  7647  elnp1st2nd  7689  prcdnql  7697  prnminu  7702  prloc  7704  genpcdl  7732  addnqprulem  7741  addlocprlemlt  7744  addlocprlemgt  7747  addlocprlem  7748  addlocpr  7749  nqprxx  7759  ltnqex  7762  addnqprlemfl  7772  addnqprlemfu  7773  appdivnq  7776  prmuloclemcalc  7778  prmuloc  7779  mullocprlem  7783  mulnqprlemfl  7788  mulnqprlemfu  7789  ltprordil  7802  ltnqpri  7807  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemdisj  7819  ltexprlemloc  7820  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  ltexpri  7826  lteupri  7830  ltaprlem  7831  recexprlemell  7835  recexprlemelu  7836  recexprlemloc  7844  recexprlempr  7845  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1u  7849  aptipr  7854  cauappcvgprlemm  7858  cauappcvgprlemlol  7860  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlemladdru  7869  cauappcvgprlem1  7872  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemm  7881  caucvgprlemlol  7883  caucvgprlemladdfu  7890  caucvgprprlemloccalc  7897  caucvgprprlemnkltj  7902  caucvgprprlemnbj  7906  caucvgprprlemml  7907  caucvgprprlemlol  7911  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  suplocexprlemss  7928  suplocexprlemru  7932  suplocexprlemlub  7937  ltsrprg  7960  caucvgsrlemasr  8003  suplocsrlemb  8019  suplocsrlem  8021  suplocsr  8022  axcaucvglemcau  8111  axpre-suploclemres  8114  negf1o  8554  apreap  8760  apreim  8776  msqge0  8789  mulge0  8792  apti  8795  apsscn  8820  mulap0bad  8832  divadddivap  8900  recnz  9566  lbzbi  9843  xadd4d  10113  ixxss1  10132  ixxss2  10133  ixxss12  10134  iccss2  10172  iccssioo2  10174  iccssico2  10175  iccen  10234  elfzole1  10384  ioom  10513  elicore  10519  flqle  10531  flqltnz  10540  addmodlteq  10653  expclzap  10819  hashennnuni  11034  zfz1isolem1  11097  hashdmprop2dom  11101  swrdsbslen  11240  ccatswrd  11244  ccatpfx  11275  recl  11407  cvg1nlemcau  11538  cvg1nlemres  11539  resqrtth  11585  fimaxre2  11781  climcl  11836  reccn2ap  11867  nnf1o  11930  summodclem3  11934  sumpr  11967  fsump1i  11987  fisumcom2  11992  fsum00  12016  fsumparts  12024  mertenslemi1  12089  prodmodclem3  12129  fprodcom2fi  12180  addsin  12296  subsin  12297  addcos  12300  subcos  12301  sinbnd2  12308  cosbnd2  12309  sin01gt0  12316  cos01gt0  12317  divgcdz  12535  divgcdnn  12539  gcdaddm  12548  bezoutlemstep  12561  dvdsgcdb  12577  dfgcd2  12578  mulgcd  12580  gcdzeq  12586  dvdsmulgcd  12589  sqgcd  12593  bezoutr  12596  lcmval  12628  lcmcllem  12632  gcddvdslcm  12638  lcmgcdlem  12642  lcmgcd  12643  lcmgcdeq  12648  lcmdvdsb  12649  mulgcddvds  12659  rpmulgcd2  12660  qredeu  12662  rpdvds  12664  isprm3  12683  divgcdodd  12708  coprm  12709  rpexp  12718  sqrt2irr  12727  qnumcl  12753  qnumdencoprm  12758  divnumden  12761  numsq  12768  phimullem  12790  eulerthlem1  12792  prmdiveq  12801  prmdivdiv  12802  hashgcdlem  12803  odzcl  12809  reumodprminv  12819  pythagtriplem19  12848  pclemub  12853  pcprendvds  12856  pcprendvds2  12857  pcpre1  12858  pcpremul  12859  pceulem  12860  pceu  12861  pczpre  12863  pczcl  12864  pcgcd1  12894  pc2dvds  12896  pcaddlem  12905  pcmpt  12909  pockthlem  12922  prmunb  12928  4sqlem7  12950  4sqlem8  12951  4sqlem9  12952  4sqlem10  12953  4sqlem14  12970  4sqlem15  12971  4sqlem16  12972  4sqlem17  12973  4sqlem18  12974  ennnfonelemg  13017  ennnfonelemf1  13032  ctiunctlemu1st  13048  nninfdclemf  13063  nninfdclemp1  13064  mgmidcl  13454  gsumfzval  13467  gsumval2  13473  mndlid  13511  prdsmndd  13524  imasmndf1  13530  dfgrp3mlem  13674  grplactf1o  13679  prdsgrpd  13685  prdsinvgd  13686  imasgrpf1  13692  subgsubm  13776  qusgrp  13812  ghmgrp1  13825  ghmf  13827  ghmnsgpreima  13849  kerf1ghm  13854  conjsubg  13857  imasrng  13962  srgdilem  13975  srgdi  13980  srglidm  13985  ringdilem  14018  ringdi  14024  ringlidm  14029  imasring  14070  imasringf1  14071  dvdsrcld  14104  unitcld  14115  unitmulcl  14120  unitnegcl  14137  rhmghm  14169  elrhmunit  14184  subrgss  14229  subrgrcl  14233  lmodvscl  14312  lmodvsdi  14318  lmodvsdir  14319  lsslsp  14436  qusring  14534  crngridl  14537  znunit  14666  znrrg  14667  psrbaglesuppg  14679  psrelbas  14682  psraddcl  14687  mplrcl  14701  uniopn  14718  restbasg  14885  cntop1  14918  cnf  14921  cnpf2  14924  lmtopcnp  14967  psmetdmdm  15041  psmetf  15042  psmet0  15044  xmetf  15067  metf  15068  blhalf  15125  xmetxpbl  15225  ioo2bl  15268  tgioo  15271  cncff  15294  rescncf  15298  cdivcncfap  15321  cnopnap  15328  divcncfap  15331  dedekindeulemeu  15339  dedekindicclemeu  15348  ivthinclemlm  15351  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthinclemdisj  15357  ivthdec  15361  ivthreinc  15362  limcimolemlt  15381  limcimo  15382  limccnpcntop  15392  limccnp2lem  15393  limccnp2cntop  15394  limccoap  15395  eldvap  15399  dvbsssg  15403  dvfgg  15405  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvcj  15426  dvfre  15427  dvrecap  15430  plyco  15476  plycj  15478  sin0pilem1  15498  sin0pilem2  15499  pilem3  15500  tanrpcl  15554  tangtx  15555  perfect  15718  lgsne0  15760  lgseisen  15796  lgsquad2lem2  15804  2sqlem8a  15844  2sqlem8  15845  structgrssvtx  15886  edguhgr  15981  umgrpredgv  15991  umgrnloop2  15995  umgr2edg  16051  wlkpropg  16135  wlkv  16137  wlkvtxeledgg  16155  wlkvtxiedgg  16157  wlk1walkdom  16170  trlsv  16193  clwwlksswrd  16206  clwwlkclwwlkn  16218  eupthv  16255  eupthseg  16261  nninfalllem1  16560  iooref1o  16588  gfsumval  16630  alsi1d  16642  alsc1d  16644