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  3165  unssad  3337  opth1  4266  opth  4267  0nelop  4278  epelg  4322  poirr  4339  brrelex1  4699  brrelex  4700  asymref  5052  soirri  5061  sotri  5062  fcnvres  5438  fun11iun  5522  elmpocl1  6116  f1od  6123  f1o2d  6125  oprssdmm  6226  smoiso  6357  tfrlem1  6363  swoer  6617  ecopovtrn  6688  ecopovtrng  6691  elmapssres  6729  pmresg  6732  mapsspm  6738  en1uniel  6860  pw2f1odc  6893  xpf1o  6902  sbthlemi9  7026  supelti  7063  supsnti  7066  supisoti  7071  ctssdccl  7172  ctfoex  7179  fodjum  7207  en2eleq  7257  djuen  7273  dftap2  7313  2omotaplemst  7320  exmidapne  7322  ccfunen  7326  dfplpq2  7416  ltbtwnnqq  7477  enq0tr  7496  elnp1st2nd  7538  prcdnql  7546  prnminu  7551  prloc  7553  genpcdl  7581  addnqprulem  7590  addlocprlemlt  7593  addlocprlemgt  7596  addlocprlem  7597  addlocpr  7598  nqprxx  7608  ltnqex  7611  addnqprlemfl  7621  addnqprlemfu  7622  appdivnq  7625  prmuloclemcalc  7627  prmuloc  7628  mullocprlem  7632  mulnqprlemfl  7637  mulnqprlemfu  7638  ltprordil  7651  ltnqpri  7656  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  ltexpri  7675  lteupri  7679  ltaprlem  7680  recexprlemell  7684  recexprlemelu  7685  recexprlemloc  7693  recexprlempr  7694  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1u  7698  aptipr  7703  cauappcvgprlemm  7707  cauappcvgprlemlol  7709  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlem1  7721  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemlol  7732  caucvgprlemladdfu  7739  caucvgprprlemloccalc  7746  caucvgprprlemnkltj  7751  caucvgprprlemnbj  7755  caucvgprprlemml  7756  caucvgprprlemlol  7760  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  suplocexprlemss  7777  suplocexprlemru  7781  suplocexprlemlub  7786  ltsrprg  7809  caucvgsrlemasr  7852  suplocsrlemb  7868  suplocsrlem  7870  suplocsr  7871  axcaucvglemcau  7960  axpre-suploclemres  7963  negf1o  8403  apreap  8608  apreim  8624  msqge0  8637  mulge0  8640  apti  8643  apsscn  8668  mulap0bad  8680  divadddivap  8748  recnz  9413  lbzbi  9684  xadd4d  9954  ixxss1  9973  ixxss2  9974  ixxss12  9975  iccss2  10013  iccssioo2  10015  iccssico2  10016  iccen  10075  elfzole1  10225  ioom  10332  elicore  10338  flqle  10350  flqltnz  10359  addmodlteq  10472  expclzap  10638  hashennnuni  10853  zfz1isolem1  10914  recl  11000  cvg1nlemcau  11131  cvg1nlemres  11132  resqrtth  11178  fimaxre2  11373  climcl  11428  reccn2ap  11459  nnf1o  11522  summodclem3  11526  sumpr  11559  fsump1i  11579  fisumcom2  11584  fsum00  11608  fsumparts  11616  mertenslemi1  11681  prodmodclem3  11721  fprodcom2fi  11772  addsin  11888  subsin  11889  addcos  11892  subcos  11893  sinbnd2  11900  cosbnd2  11901  sin01gt0  11908  cos01gt0  11909  divgcdz  12111  divgcdnn  12115  gcdaddm  12124  bezoutlemstep  12137  dvdsgcdb  12153  dfgcd2  12154  mulgcd  12156  gcdzeq  12162  dvdsmulgcd  12165  sqgcd  12169  bezoutr  12172  lcmval  12204  lcmcllem  12208  gcddvdslcm  12214  lcmgcdlem  12218  lcmgcd  12219  lcmgcdeq  12224  lcmdvdsb  12225  mulgcddvds  12235  rpmulgcd2  12236  qredeu  12238  rpdvds  12240  isprm3  12259  divgcdodd  12284  coprm  12285  rpexp  12294  sqrt2irr  12303  qnumcl  12329  qnumdencoprm  12334  divnumden  12337  numsq  12344  phimullem  12366  eulerthlem1  12368  prmdiveq  12377  prmdivdiv  12378  hashgcdlem  12379  odzcl  12384  reumodprminv  12394  pythagtriplem19  12423  pclemub  12428  pcprendvds  12431  pcprendvds2  12432  pcpre1  12433  pcpremul  12434  pceulem  12435  pceu  12436  pczpre  12438  pczcl  12439  pcgcd1  12469  pc2dvds  12471  pcaddlem  12480  pcmpt  12484  pockthlem  12497  prmunb  12503  4sqlem7  12525  4sqlem8  12526  4sqlem9  12527  4sqlem10  12528  4sqlem14  12545  4sqlem15  12546  4sqlem16  12547  4sqlem17  12548  4sqlem18  12549  ennnfonelemg  12563  ennnfonelemf1  12578  ctiunctlemu1st  12594  nninfdclemf  12609  nninfdclemp1  12610  mgmidcl  12964  gsumfzval  12977  gsumval2  12983  mndlid  13019  dfgrp3mlem  13173  grplactf1o  13178  imasgrpf1  13185  subgsubm  13269  qusgrp  13305  ghmgrp1  13318  ghmf  13320  ghmnsgpreima  13342  kerf1ghm  13347  conjsubg  13350  imasrng  13455  srgdilem  13468  srgdi  13473  srglidm  13478  ringdilem  13511  ringdi  13517  ringlidm  13522  imasring  13563  imasringf1  13564  dvdsrcld  13596  unitcld  13607  unitmulcl  13612  unitnegcl  13629  rhmghm  13661  elrhmunit  13676  subrgss  13721  subrgrcl  13725  lmodvscl  13804  lmodvsdi  13810  lmodvsdir  13811  lsslsp  13928  qusring  14026  crngridl  14029  znunit  14158  znrrg  14159  psrbaglesuppg  14169  psrelbas  14171  psraddcl  14175  uniopn  14180  restbasg  14347  cntop1  14380  cnf  14383  cnpf2  14386  lmtopcnp  14429  psmetdmdm  14503  psmetf  14504  psmet0  14506  xmetf  14529  metf  14530  blhalf  14587  xmetxpbl  14687  ioo2bl  14730  tgioo  14733  cncff  14756  rescncf  14760  cdivcncfap  14783  cnopnap  14790  divcncfap  14793  dedekindeulemeu  14801  dedekindicclemeu  14810  ivthinclemlm  14813  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthinclemdisj  14819  ivthdec  14823  ivthreinc  14824  limcimolemlt  14843  limcimo  14844  limccnpcntop  14854  limccnp2lem  14855  limccnp2cntop  14856  limccoap  14857  eldvap  14861  dvbsssg  14865  dvfgg  14867  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcj  14888  dvfre  14889  dvrecap  14892  plyco  14937  plycj  14939  sin0pilem1  14957  sin0pilem2  14958  pilem3  14959  tanrpcl  15013  tangtx  15014  lgsne0  15195  lgseisen  15231  lgsquad2lem2  15239  2sqlem8a  15279  2sqlem8  15280  nninfalllem1  15568  iooref1o  15594  alsi1d  15641  alsc1d  15643