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  3208  unssad  3381  opth1  4322  opth  4323  0nelop  4334  epelg  4381  poirr  4398  brrelex1  4758  brrelex  4759  asymref  5114  soirri  5123  sotri  5124  ffdmd  5497  fcnvres  5511  fun11iun  5595  funopsn  5819  elmpocl1  6207  f1od  6215  f1o2d  6217  oprssdmm  6323  smoiso  6454  tfrlem1  6460  swoer  6716  ecopovtrn  6787  ecopovtrng  6790  elmapssres  6828  pmresg  6831  mapsspm  6837  en1uniel  6964  pw2f1odc  7004  xpf1o  7013  sbthlemi9  7140  supelti  7177  supsnti  7180  supisoti  7185  ctssdccl  7286  ctfoex  7293  fodjum  7321  en2eleq  7381  djuen  7401  pw1if  7418  dftap2  7445  2omotaplemst  7452  exmidapne  7454  ccfunen  7458  dfplpq2  7549  ltbtwnnqq  7610  enq0tr  7629  elnp1st2nd  7671  prcdnql  7679  prnminu  7684  prloc  7686  genpcdl  7714  addnqprulem  7723  addlocprlemlt  7726  addlocprlemgt  7729  addlocprlem  7730  addlocpr  7731  nqprxx  7741  ltnqex  7744  addnqprlemfl  7754  addnqprlemfu  7755  appdivnq  7758  prmuloclemcalc  7760  prmuloc  7761  mullocprlem  7765  mulnqprlemfl  7770  mulnqprlemfu  7771  ltprordil  7784  ltnqpri  7789  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemlol  7797  ltexprlemopu  7798  ltexprlemupu  7799  ltexprlemdisj  7801  ltexprlemloc  7802  ltexprlemfl  7804  ltexprlemrl  7805  ltexprlemfu  7806  ltexprlemru  7807  ltexpri  7808  lteupri  7812  ltaprlem  7813  recexprlemell  7817  recexprlemelu  7818  recexprlemloc  7826  recexprlempr  7827  recexprlem1ssl  7828  recexprlem1ssu  7829  recexprlemss1u  7831  aptipr  7836  cauappcvgprlemm  7840  cauappcvgprlemlol  7842  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlemladdru  7851  cauappcvgprlem1  7854  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemm  7863  caucvgprlemlol  7865  caucvgprlemladdfu  7872  caucvgprprlemloccalc  7879  caucvgprprlemnkltj  7884  caucvgprprlemnbj  7888  caucvgprprlemml  7889  caucvgprprlemlol  7893  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  suplocexprlemss  7910  suplocexprlemru  7914  suplocexprlemlub  7919  ltsrprg  7942  caucvgsrlemasr  7985  suplocsrlemb  8001  suplocsrlem  8003  suplocsr  8004  axcaucvglemcau  8093  axpre-suploclemres  8096  negf1o  8536  apreap  8742  apreim  8758  msqge0  8771  mulge0  8774  apti  8777  apsscn  8802  mulap0bad  8814  divadddivap  8882  recnz  9548  lbzbi  9819  xadd4d  10089  ixxss1  10108  ixxss2  10109  ixxss12  10110  iccss2  10148  iccssioo2  10150  iccssico2  10151  iccen  10210  elfzole1  10360  ioom  10488  elicore  10494  flqle  10506  flqltnz  10515  addmodlteq  10628  expclzap  10794  hashennnuni  11009  zfz1isolem1  11070  hashdmprop2dom  11074  swrdsbslen  11206  ccatswrd  11210  ccatpfx  11241  recl  11372  cvg1nlemcau  11503  cvg1nlemres  11504  resqrtth  11550  fimaxre2  11746  climcl  11801  reccn2ap  11832  nnf1o  11895  summodclem3  11899  sumpr  11932  fsump1i  11952  fisumcom2  11957  fsum00  11981  fsumparts  11989  mertenslemi1  12054  prodmodclem3  12094  fprodcom2fi  12145  addsin  12261  subsin  12262  addcos  12265  subcos  12266  sinbnd2  12273  cosbnd2  12274  sin01gt0  12281  cos01gt0  12282  divgcdz  12500  divgcdnn  12504  gcdaddm  12513  bezoutlemstep  12526  dvdsgcdb  12542  dfgcd2  12543  mulgcd  12545  gcdzeq  12551  dvdsmulgcd  12554  sqgcd  12558  bezoutr  12561  lcmval  12593  lcmcllem  12597  gcddvdslcm  12603  lcmgcdlem  12607  lcmgcd  12608  lcmgcdeq  12613  lcmdvdsb  12614  mulgcddvds  12624  rpmulgcd2  12625  qredeu  12627  rpdvds  12629  isprm3  12648  divgcdodd  12673  coprm  12674  rpexp  12683  sqrt2irr  12692  qnumcl  12718  qnumdencoprm  12723  divnumden  12726  numsq  12733  phimullem  12755  eulerthlem1  12757  prmdiveq  12766  prmdivdiv  12767  hashgcdlem  12768  odzcl  12774  reumodprminv  12784  pythagtriplem19  12813  pclemub  12818  pcprendvds  12821  pcprendvds2  12822  pcpre1  12823  pcpremul  12824  pceulem  12825  pceu  12826  pczpre  12828  pczcl  12829  pcgcd1  12859  pc2dvds  12861  pcaddlem  12870  pcmpt  12874  pockthlem  12887  prmunb  12893  4sqlem7  12915  4sqlem8  12916  4sqlem9  12917  4sqlem10  12918  4sqlem14  12935  4sqlem15  12936  4sqlem16  12937  4sqlem17  12938  4sqlem18  12939  ennnfonelemg  12982  ennnfonelemf1  12997  ctiunctlemu1st  13013  nninfdclemf  13028  nninfdclemp1  13029  mgmidcl  13419  gsumfzval  13432  gsumval2  13438  mndlid  13476  prdsmndd  13489  imasmndf1  13495  dfgrp3mlem  13639  grplactf1o  13644  prdsgrpd  13650  prdsinvgd  13651  imasgrpf1  13657  subgsubm  13741  qusgrp  13777  ghmgrp1  13790  ghmf  13792  ghmnsgpreima  13814  kerf1ghm  13819  conjsubg  13822  imasrng  13927  srgdilem  13940  srgdi  13945  srglidm  13950  ringdilem  13983  ringdi  13989  ringlidm  13994  imasring  14035  imasringf1  14036  dvdsrcld  14069  unitcld  14080  unitmulcl  14085  unitnegcl  14102  rhmghm  14134  elrhmunit  14149  subrgss  14194  subrgrcl  14198  lmodvscl  14277  lmodvsdi  14283  lmodvsdir  14284  lsslsp  14401  qusring  14499  crngridl  14502  znunit  14631  znrrg  14632  psrbaglesuppg  14644  psrelbas  14647  psraddcl  14652  mplrcl  14666  uniopn  14683  restbasg  14850  cntop1  14883  cnf  14886  cnpf2  14889  lmtopcnp  14932  psmetdmdm  15006  psmetf  15007  psmet0  15009  xmetf  15032  metf  15033  blhalf  15090  xmetxpbl  15190  ioo2bl  15233  tgioo  15236  cncff  15259  rescncf  15263  cdivcncfap  15286  cnopnap  15293  divcncfap  15296  dedekindeulemeu  15304  dedekindicclemeu  15313  ivthinclemlm  15316  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthinclemdisj  15322  ivthdec  15326  ivthreinc  15327  limcimolemlt  15346  limcimo  15347  limccnpcntop  15357  limccnp2lem  15358  limccnp2cntop  15359  limccoap  15360  eldvap  15364  dvbsssg  15368  dvfgg  15370  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcj  15391  dvfre  15392  dvrecap  15395  plyco  15441  plycj  15443  sin0pilem1  15463  sin0pilem2  15464  pilem3  15465  tanrpcl  15519  tangtx  15520  perfect  15683  lgsne0  15725  lgseisen  15761  lgsquad2lem2  15769  2sqlem8a  15809  2sqlem8  15810  structgrssvtx  15851  edguhgr  15943  umgrpredgv  15953  umgrnloop2  15957  umgr2edg  16013  wlkpropg  16045  wlkv  16047  wlkvtxeledgg  16065  wlkvtxiedgg  16067  wlk1walkdom  16080  trlsv  16103  nninfalllem1  16404  iooref1o  16432  alsi1d  16479  alsc1d  16481