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  simplld  528  simplrd  530  simprld  532  simp1  1023  eldifad  3211  unssad  3384  opth1  4328  opth  4329  0nelop  4340  epelg  4387  poirr  4404  brrelex1  4765  brrelex  4766  asymref  5122  soirri  5131  sotri  5132  ffdmd  5506  fcnvres  5520  fun11iun  5604  funopsn  5830  elmpocl1  6218  f1od  6226  f1o2d  6228  oprssdmm  6334  elmpom  6403  smoiso  6468  tfrlem1  6474  swoer  6730  ecopovtrn  6801  ecopovtrng  6804  elmapssres  6842  pmresg  6845  mapsspm  6851  en1uniel  6978  pw2f1odc  7021  xpf1o  7030  sbthlemi9  7164  supelti  7201  supsnti  7204  supisoti  7209  ctssdccl  7310  ctfoex  7317  fodjum  7345  en2eleq  7406  djuen  7426  pw1if  7443  dftap2  7470  2omotaplemst  7477  exmidapne  7479  ccfunen  7483  dfplpq2  7574  ltbtwnnqq  7635  enq0tr  7654  elnp1st2nd  7696  prcdnql  7704  prnminu  7709  prloc  7711  genpcdl  7739  addnqprulem  7748  addlocprlemlt  7751  addlocprlemgt  7754  addlocprlem  7755  addlocpr  7756  nqprxx  7766  ltnqex  7769  addnqprlemfl  7779  addnqprlemfu  7780  appdivnq  7783  prmuloclemcalc  7785  prmuloc  7786  mullocprlem  7790  mulnqprlemfl  7795  mulnqprlemfu  7796  ltprordil  7809  ltnqpri  7814  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  ltexpri  7833  lteupri  7837  ltaprlem  7838  recexprlemell  7842  recexprlemelu  7843  recexprlemloc  7851  recexprlempr  7852  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1u  7856  aptipr  7861  cauappcvgprlemm  7865  cauappcvgprlemlol  7867  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemlol  7890  caucvgprlemladdfu  7897  caucvgprprlemloccalc  7904  caucvgprprlemnkltj  7909  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemlol  7918  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  suplocexprlemss  7935  suplocexprlemru  7939  suplocexprlemlub  7944  ltsrprg  7967  caucvgsrlemasr  8010  suplocsrlemb  8026  suplocsrlem  8028  suplocsr  8029  axcaucvglemcau  8118  axpre-suploclemres  8121  negf1o  8561  apreap  8767  apreim  8783  msqge0  8796  mulge0  8799  apti  8802  apsscn  8827  mulap0bad  8839  divadddivap  8907  recnz  9573  lbzbi  9850  xadd4d  10120  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iccssioo2  10181  iccssico2  10182  iccen  10241  elfzole1  10391  ioom  10521  elicore  10527  flqle  10539  flqltnz  10548  addmodlteq  10661  expclzap  10827  hashennnuni  11042  zfz1isolem1  11105  hashdmprop2dom  11109  swrdsbslen  11251  ccatswrd  11255  ccatpfx  11286  recl  11418  cvg1nlemcau  11549  cvg1nlemres  11550  resqrtth  11596  fimaxre2  11792  climcl  11847  reccn2ap  11878  nnf1o  11942  summodclem3  11946  sumpr  11979  fsump1i  11999  fisumcom2  12004  fsum00  12028  fsumparts  12036  mertenslemi1  12101  prodmodclem3  12141  fprodcom2fi  12192  addsin  12308  subsin  12309  addcos  12312  subcos  12313  sinbnd2  12320  cosbnd2  12321  sin01gt0  12328  cos01gt0  12329  divgcdz  12547  divgcdnn  12551  gcdaddm  12560  bezoutlemstep  12573  dvdsgcdb  12589  dfgcd2  12590  mulgcd  12592  gcdzeq  12598  dvdsmulgcd  12601  sqgcd  12605  bezoutr  12608  lcmval  12640  lcmcllem  12644  gcddvdslcm  12650  lcmgcdlem  12654  lcmgcd  12655  lcmgcdeq  12660  lcmdvdsb  12661  mulgcddvds  12671  rpmulgcd2  12672  qredeu  12674  rpdvds  12676  isprm3  12695  divgcdodd  12720  coprm  12721  rpexp  12730  sqrt2irr  12739  qnumcl  12765  qnumdencoprm  12770  divnumden  12773  numsq  12780  phimullem  12802  eulerthlem1  12804  prmdiveq  12813  prmdivdiv  12814  hashgcdlem  12815  odzcl  12821  reumodprminv  12831  pythagtriplem19  12860  pclemub  12865  pcprendvds  12868  pcprendvds2  12869  pcpre1  12870  pcpremul  12871  pceulem  12872  pceu  12873  pczpre  12875  pczcl  12876  pcgcd1  12906  pc2dvds  12908  pcaddlem  12917  pcmpt  12921  pockthlem  12934  prmunb  12940  4sqlem7  12962  4sqlem8  12963  4sqlem9  12964  4sqlem10  12965  4sqlem14  12982  4sqlem15  12983  4sqlem16  12984  4sqlem17  12985  4sqlem18  12986  ennnfonelemg  13029  ennnfonelemf1  13044  ctiunctlemu1st  13060  nninfdclemf  13075  nninfdclemp1  13076  mgmidcl  13466  gsumfzval  13479  gsumval2  13485  mndlid  13523  prdsmndd  13536  imasmndf1  13542  dfgrp3mlem  13686  grplactf1o  13691  prdsgrpd  13697  prdsinvgd  13698  imasgrpf1  13704  subgsubm  13788  qusgrp  13824  ghmgrp1  13837  ghmf  13839  ghmnsgpreima  13861  kerf1ghm  13866  conjsubg  13869  gsumsplit0  13938  imasrng  13975  srgdilem  13988  srgdi  13993  srglidm  13998  ringdilem  14031  ringdi  14037  ringlidm  14042  imasring  14083  imasringf1  14084  dvdsrcld  14117  unitcld  14128  unitmulcl  14133  unitnegcl  14150  rhmghm  14182  elrhmunit  14197  subrgss  14242  subrgrcl  14246  lmodvscl  14325  lmodvsdi  14331  lmodvsdir  14332  lsslsp  14449  qusring  14547  crngridl  14550  znunit  14679  znrrg  14680  psrbaglesuppg  14692  psrelbas  14695  psraddcl  14700  mplrcl  14714  uniopn  14731  restbasg  14898  cntop1  14931  cnf  14934  cnpf2  14937  lmtopcnp  14980  psmetdmdm  15054  psmetf  15055  psmet0  15057  xmetf  15080  metf  15081  blhalf  15138  xmetxpbl  15238  ioo2bl  15281  tgioo  15284  cncff  15307  rescncf  15311  cdivcncfap  15334  cnopnap  15341  divcncfap  15344  dedekindeulemeu  15352  dedekindicclemeu  15361  ivthinclemlm  15364  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthinclemdisj  15370  ivthdec  15374  ivthreinc  15375  limcimolemlt  15394  limcimo  15395  limccnpcntop  15405  limccnp2lem  15406  limccnp2cntop  15407  limccoap  15408  eldvap  15412  dvbsssg  15416  dvfgg  15418  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437  dvcj  15439  dvfre  15440  dvrecap  15443  plyco  15489  plycj  15491  sin0pilem1  15511  sin0pilem2  15512  pilem3  15513  tanrpcl  15567  tangtx  15568  perfect  15731  lgsne0  15773  lgseisen  15809  lgsquad2lem2  15817  2sqlem8a  15857  2sqlem8  15858  structgrssvtx  15899  edguhgr  15994  umgrpredgv  16004  umgrnloop2  16008  umgr2edg  16064  subuhgr  16129  subumgr  16131  subusgr  16132  wlkpropg  16181  wlkv  16183  wlkvtxeledgg  16201  wlkvtxiedgg  16203  wlk1walkdom  16216  trlsv  16241  clwwlksswrd  16254  clwwlkclwwlkn  16266  eupthv  16303  eupthseg  16309  eupth2lem3lem3fi  16327  eupth2lem3lem4fi  16330  eupth2lemsfi  16335  eulerpathprum  16337  nninfalllem1  16636  iooref1o  16664  gfsumval  16706  alsi1d  16721  alsc1d  16723