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  997  eldifad  3141  unssad  3313  opth1  4237  opth  4238  0nelop  4249  epelg  4291  poirr  4308  brrelex1  4666  brrelex  4667  asymref  5015  soirri  5024  sotri  5025  fcnvres  5400  fun11iun  5483  elmpocl1  6070  f1od  6074  f1o2d  6076  oprssdmm  6172  smoiso  6303  tfrlem1  6309  swoer  6563  ecopovtrn  6632  ecopovtrng  6635  elmapssres  6673  pmresg  6676  mapsspm  6682  en1uniel  6804  xpf1o  6844  sbthlemi9  6964  supelti  7001  supsnti  7004  supisoti  7009  ctssdccl  7110  ctfoex  7117  fodjum  7144  en2eleq  7194  djuen  7210  dftap2  7250  2omotaplemst  7257  exmidapne  7259  ccfunen  7263  dfplpq2  7353  ltbtwnnqq  7414  enq0tr  7433  elnp1st2nd  7475  prcdnql  7483  prnminu  7488  prloc  7490  genpcdl  7518  addnqprulem  7527  addlocprlemlt  7530  addlocprlemgt  7533  addlocprlem  7534  addlocpr  7535  nqprxx  7545  ltnqex  7548  addnqprlemfl  7558  addnqprlemfu  7559  appdivnq  7562  prmuloclemcalc  7564  prmuloc  7565  mullocprlem  7569  mulnqprlemfl  7574  mulnqprlemfu  7575  ltprordil  7588  ltnqpri  7593  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  ltexpri  7612  lteupri  7616  ltaprlem  7617  recexprlemell  7621  recexprlemelu  7622  recexprlemloc  7630  recexprlempr  7631  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1u  7635  aptipr  7640  cauappcvgprlemm  7644  cauappcvgprlemlol  7646  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlem1  7658  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemlol  7669  caucvgprlemladdfu  7676  caucvgprprlemloccalc  7683  caucvgprprlemnkltj  7688  caucvgprprlemnbj  7692  caucvgprprlemml  7693  caucvgprprlemlol  7697  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  suplocexprlemss  7714  suplocexprlemru  7718  suplocexprlemlub  7723  ltsrprg  7746  caucvgsrlemasr  7789  suplocsrlemb  7805  suplocsrlem  7807  suplocsr  7808  axcaucvglemcau  7897  axpre-suploclemres  7900  negf1o  8339  apreap  8544  apreim  8560  msqge0  8573  mulge0  8576  apti  8579  apsscn  8604  mulap0bad  8616  divadddivap  8684  recnz  9346  lbzbi  9616  xadd4d  9885  ixxss1  9904  ixxss2  9905  ixxss12  9906  iccss2  9944  iccssioo2  9946  iccssico2  9947  iccen  10006  elfzole1  10155  ioom  10261  elicore  10267  flqle  10278  flqltnz  10287  addmodlteq  10398  expclzap  10545  hashennnuni  10759  zfz1isolem1  10820  recl  10862  cvg1nlemcau  10993  cvg1nlemres  10994  resqrtth  11040  fimaxre2  11235  climcl  11290  reccn2ap  11321  nnf1o  11384  summodclem3  11388  sumpr  11421  fsump1i  11441  fisumcom2  11446  fsum00  11470  fsumparts  11478  mertenslemi1  11543  prodmodclem3  11583  fprodcom2fi  11634  addsin  11750  subsin  11751  addcos  11754  subcos  11755  sinbnd2  11762  cosbnd2  11763  sin01gt0  11769  cos01gt0  11770  divgcdz  11972  divgcdnn  11976  gcdaddm  11985  bezoutlemstep  11998  dvdsgcdb  12014  dfgcd2  12015  mulgcd  12017  gcdzeq  12023  dvdsmulgcd  12026  sqgcd  12030  bezoutr  12033  lcmval  12063  lcmcllem  12067  gcddvdslcm  12073  lcmgcdlem  12077  lcmgcd  12078  lcmgcdeq  12083  lcmdvdsb  12084  mulgcddvds  12094  rpmulgcd2  12095  qredeu  12097  rpdvds  12099  isprm3  12118  divgcdodd  12143  coprm  12144  rpexp  12153  sqrt2irr  12162  qnumcl  12188  qnumdencoprm  12193  divnumden  12196  numsq  12203  phimullem  12225  eulerthlem1  12227  prmdiveq  12236  prmdivdiv  12237  hashgcdlem  12238  odzcl  12243  reumodprminv  12253  pythagtriplem19  12282  pclemub  12287  pcprendvds  12290  pcprendvds2  12291  pcpre1  12292  pcpremul  12293  pceulem  12294  pceu  12295  pczpre  12297  pczcl  12298  pcgcd1  12327  pc2dvds  12329  pcaddlem  12338  pcmpt  12341  pockthlem  12354  prmunb  12360  4sqlem7  12382  4sqlem8  12383  4sqlem9  12384  4sqlem10  12385  ennnfonelemg  12404  ennnfonelemf1  12419  ctiunctlemu1st  12435  nninfdclemf  12450  nninfdclemp1  12451  mgmidcl  12797  mndlid  12836  dfgrp3mlem  12968  grplactf1o  12973  subgsubm  13056  srgdilem  13152  srgdi  13157  srglidm  13162  ringdilem  13195  ringdi  13201  ringlidm  13206  dvdsrcld  13266  unitcld  13277  unitmulcl  13282  unitnegcl  13299  subrgss  13343  subrgrcl  13347  lmodvscl  13395  lmodvsdi  13401  lmodvsdir  13402  uniopn  13504  restbasg  13671  cntop1  13704  cnf  13707  cnpf2  13710  lmtopcnp  13753  psmetdmdm  13827  psmetf  13828  psmet0  13830  xmetf  13853  metf  13854  blhalf  13911  xmetxpbl  14011  ioo2bl  14046  tgioo  14049  cncff  14067  rescncf  14071  cdivcncfap  14090  cnopnap  14097  dedekindeulemeu  14103  dedekindicclemeu  14112  ivthinclemlm  14115  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthinclemdisj  14121  ivthdec  14125  limcimolemlt  14136  limcimo  14137  limccnpcntop  14147  limccnp2lem  14148  limccnp2cntop  14149  limccoap  14150  eldvap  14154  dvbsssg  14158  dvfgg  14160  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcj  14176  dvfre  14177  dvrecap  14180  sin0pilem1  14205  sin0pilem2  14206  pilem3  14207  tanrpcl  14261  tangtx  14262  lgsne0  14442  2sqlem8a  14472  2sqlem8  14473  nninfalllem1  14760  iooref1o  14785  alsi1d  14831  alsc1d  14833