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  3140  unssad  3312  opth1  4236  opth  4237  0nelop  4248  epelg  4290  poirr  4307  brrelex1  4665  brrelex  4666  asymref  5014  soirri  5023  sotri  5024  fcnvres  5399  fun11iun  5482  elmpocl1  6069  f1od  6073  f1o2d  6075  oprssdmm  6171  smoiso  6302  tfrlem1  6308  swoer  6562  ecopovtrn  6631  ecopovtrng  6634  elmapssres  6672  pmresg  6675  mapsspm  6681  en1uniel  6803  xpf1o  6843  sbthlemi9  6963  supelti  7000  supsnti  7003  supisoti  7008  ctssdccl  7109  ctfoex  7116  fodjum  7143  en2eleq  7193  djuen  7209  dftap2  7249  2omotaplemst  7256  exmidapne  7258  ccfunen  7262  dfplpq2  7352  ltbtwnnqq  7413  enq0tr  7432  elnp1st2nd  7474  prcdnql  7482  prnminu  7487  prloc  7489  genpcdl  7517  addnqprulem  7526  addlocprlemlt  7529  addlocprlemgt  7532  addlocprlem  7533  addlocpr  7534  nqprxx  7544  ltnqex  7547  addnqprlemfl  7557  addnqprlemfu  7558  appdivnq  7561  prmuloclemcalc  7563  prmuloc  7564  mullocprlem  7568  mulnqprlemfl  7573  mulnqprlemfu  7574  ltprordil  7587  ltnqpri  7592  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  ltexprlemdisj  7604  ltexprlemloc  7605  ltexprlemfl  7607  ltexprlemrl  7608  ltexprlemfu  7609  ltexprlemru  7610  ltexpri  7611  lteupri  7615  ltaprlem  7616  recexprlemell  7620  recexprlemelu  7621  recexprlemloc  7629  recexprlempr  7630  recexprlem1ssl  7631  recexprlem1ssu  7632  recexprlemss1u  7634  aptipr  7639  cauappcvgprlemm  7643  cauappcvgprlemlol  7645  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlem1  7657  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemlol  7668  caucvgprlemladdfu  7675  caucvgprprlemloccalc  7682  caucvgprprlemnkltj  7687  caucvgprprlemnbj  7691  caucvgprprlemml  7692  caucvgprprlemlol  7696  caucvgprprlemloc  7701  caucvgprprlemexbt  7704  suplocexprlemss  7713  suplocexprlemru  7717  suplocexprlemlub  7722  ltsrprg  7745  caucvgsrlemasr  7788  suplocsrlemb  7804  suplocsrlem  7806  suplocsr  7807  axcaucvglemcau  7896  axpre-suploclemres  7899  negf1o  8338  apreap  8543  apreim  8559  msqge0  8572  mulge0  8575  apti  8578  apsscn  8603  mulap0bad  8615  divadddivap  8683  recnz  9345  lbzbi  9615  xadd4d  9884  ixxss1  9903  ixxss2  9904  ixxss12  9905  iccss2  9943  iccssioo2  9945  iccssico2  9946  iccen  10005  elfzole1  10154  ioom  10260  elicore  10266  flqle  10277  flqltnz  10286  addmodlteq  10397  expclzap  10544  hashennnuni  10758  zfz1isolem1  10819  recl  10861  cvg1nlemcau  10992  cvg1nlemres  10993  resqrtth  11039  fimaxre2  11234  climcl  11289  reccn2ap  11320  nnf1o  11383  summodclem3  11387  sumpr  11420  fsump1i  11440  fisumcom2  11445  fsum00  11469  fsumparts  11477  mertenslemi1  11542  prodmodclem3  11582  fprodcom2fi  11633  addsin  11749  subsin  11750  addcos  11753  subcos  11754  sinbnd2  11761  cosbnd2  11762  sin01gt0  11768  cos01gt0  11769  divgcdz  11971  divgcdnn  11975  gcdaddm  11984  bezoutlemstep  11997  dvdsgcdb  12013  dfgcd2  12014  mulgcd  12016  gcdzeq  12022  dvdsmulgcd  12025  sqgcd  12029  bezoutr  12032  lcmval  12062  lcmcllem  12066  gcddvdslcm  12072  lcmgcdlem  12076  lcmgcd  12077  lcmgcdeq  12082  lcmdvdsb  12083  mulgcddvds  12093  rpmulgcd2  12094  qredeu  12096  rpdvds  12098  isprm3  12117  divgcdodd  12142  coprm  12143  rpexp  12152  sqrt2irr  12161  qnumcl  12187  qnumdencoprm  12192  divnumden  12195  numsq  12202  phimullem  12224  eulerthlem1  12226  prmdiveq  12235  prmdivdiv  12236  hashgcdlem  12237  odzcl  12242  reumodprminv  12252  pythagtriplem19  12281  pclemub  12286  pcprendvds  12289  pcprendvds2  12290  pcpre1  12291  pcpremul  12292  pceulem  12293  pceu  12294  pczpre  12296  pczcl  12297  pcgcd1  12326  pc2dvds  12328  pcaddlem  12337  pcmpt  12340  pockthlem  12353  prmunb  12359  4sqlem7  12381  4sqlem8  12382  4sqlem9  12383  4sqlem10  12384  ennnfonelemg  12403  ennnfonelemf1  12418  ctiunctlemu1st  12434  nninfdclemf  12449  nninfdclemp1  12450  mgmidcl  12796  mndlid  12835  dfgrp3mlem  12967  grplactf1o  12972  subgsubm  13054  srgdilem  13150  srgdi  13155  srglidm  13160  ringdilem  13193  ringdi  13199  ringlidm  13204  dvdsrcld  13264  unitcld  13275  unitmulcl  13280  unitnegcl  13297  subrgss  13341  subrgrcl  13345  lmodvscl  13393  lmodvsdi  13399  lmodvsdir  13400  uniopn  13471  restbasg  13638  cntop1  13671  cnf  13674  cnpf2  13677  lmtopcnp  13720  psmetdmdm  13794  psmetf  13795  psmet0  13797  xmetf  13820  metf  13821  blhalf  13878  xmetxpbl  13978  ioo2bl  14013  tgioo  14016  cncff  14034  rescncf  14038  cdivcncfap  14057  cnopnap  14064  dedekindeulemeu  14070  dedekindicclemeu  14079  ivthinclemlm  14082  ivthinclemlopn  14084  ivthinclemuopn  14086  ivthinclemdisj  14088  ivthdec  14092  limcimolemlt  14103  limcimo  14104  limccnpcntop  14114  limccnp2lem  14115  limccnp2cntop  14116  limccoap  14117  eldvap  14121  dvbsssg  14125  dvfgg  14127  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcj  14143  dvfre  14144  dvrecap  14147  sin0pilem1  14172  sin0pilem2  14173  pilem3  14174  tanrpcl  14228  tangtx  14229  lgsne0  14409  2sqlem8a  14439  2sqlem8  14440  nninfalllem1  14727  iooref1o  14752  alsi1d  14798  alsc1d  14800