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  4321  opth  4322  0nelop  4333  epelg  4378  poirr  4395  brrelex1  4755  brrelex  4756  asymref  5110  soirri  5119  sotri  5120  ffdmd  5491  fcnvres  5505  fun11iun  5589  funopsn  5810  elmpocl1  6192  f1od  6199  f1o2d  6201  oprssdmm  6307  smoiso  6438  tfrlem1  6444  swoer  6698  ecopovtrn  6769  ecopovtrng  6772  elmapssres  6810  pmresg  6813  mapsspm  6819  en1uniel  6946  pw2f1odc  6984  xpf1o  6993  sbthlemi9  7120  supelti  7157  supsnti  7160  supisoti  7165  ctssdccl  7266  ctfoex  7273  fodjum  7301  en2eleq  7361  djuen  7381  pw1if  7398  dftap2  7425  2omotaplemst  7432  exmidapne  7434  ccfunen  7438  dfplpq2  7529  ltbtwnnqq  7590  enq0tr  7609  elnp1st2nd  7651  prcdnql  7659  prnminu  7664  prloc  7666  genpcdl  7694  addnqprulem  7703  addlocprlemlt  7706  addlocprlemgt  7709  addlocprlem  7710  addlocpr  7711  nqprxx  7721  ltnqex  7724  addnqprlemfl  7734  addnqprlemfu  7735  appdivnq  7738  prmuloclemcalc  7740  prmuloc  7741  mullocprlem  7745  mulnqprlemfl  7750  mulnqprlemfu  7751  ltprordil  7764  ltnqpri  7769  ltexprlemm  7775  ltexprlemopl  7776  ltexprlemlol  7777  ltexprlemopu  7778  ltexprlemupu  7779  ltexprlemdisj  7781  ltexprlemloc  7782  ltexprlemfl  7784  ltexprlemrl  7785  ltexprlemfu  7786  ltexprlemru  7787  ltexpri  7788  lteupri  7792  ltaprlem  7793  recexprlemell  7797  recexprlemelu  7798  recexprlemloc  7806  recexprlempr  7807  recexprlem1ssl  7808  recexprlem1ssu  7809  recexprlemss1u  7811  aptipr  7816  cauappcvgprlemm  7820  cauappcvgprlemlol  7822  cauappcvgprlemladdfu  7829  cauappcvgprlemladdfl  7830  cauappcvgprlemladdru  7831  cauappcvgprlem1  7834  caucvgprlemnkj  7841  caucvgprlemnbj  7842  caucvgprlemm  7843  caucvgprlemlol  7845  caucvgprlemladdfu  7852  caucvgprprlemloccalc  7859  caucvgprprlemnkltj  7864  caucvgprprlemnbj  7868  caucvgprprlemml  7869  caucvgprprlemlol  7873  caucvgprprlemloc  7878  caucvgprprlemexbt  7881  suplocexprlemss  7890  suplocexprlemru  7894  suplocexprlemlub  7899  ltsrprg  7922  caucvgsrlemasr  7965  suplocsrlemb  7981  suplocsrlem  7983  suplocsr  7984  axcaucvglemcau  8073  axpre-suploclemres  8076  negf1o  8516  apreap  8722  apreim  8738  msqge0  8751  mulge0  8754  apti  8757  apsscn  8782  mulap0bad  8794  divadddivap  8862  recnz  9528  lbzbi  9799  xadd4d  10069  ixxss1  10088  ixxss2  10089  ixxss12  10090  iccss2  10128  iccssioo2  10130  iccssico2  10131  iccen  10190  elfzole1  10340  ioom  10467  elicore  10473  flqle  10485  flqltnz  10494  addmodlteq  10607  expclzap  10773  hashennnuni  10988  zfz1isolem1  11049  hashdmprop2dom  11053  swrdsbslen  11184  ccatswrd  11188  ccatpfx  11219  recl  11350  cvg1nlemcau  11481  cvg1nlemres  11482  resqrtth  11528  fimaxre2  11724  climcl  11779  reccn2ap  11810  nnf1o  11873  summodclem3  11877  sumpr  11910  fsump1i  11930  fisumcom2  11935  fsum00  11959  fsumparts  11967  mertenslemi1  12032  prodmodclem3  12072  fprodcom2fi  12123  addsin  12239  subsin  12240  addcos  12243  subcos  12244  sinbnd2  12251  cosbnd2  12252  sin01gt0  12259  cos01gt0  12260  divgcdz  12478  divgcdnn  12482  gcdaddm  12491  bezoutlemstep  12504  dvdsgcdb  12520  dfgcd2  12521  mulgcd  12523  gcdzeq  12529  dvdsmulgcd  12532  sqgcd  12536  bezoutr  12539  lcmval  12571  lcmcllem  12575  gcddvdslcm  12581  lcmgcdlem  12585  lcmgcd  12586  lcmgcdeq  12591  lcmdvdsb  12592  mulgcddvds  12602  rpmulgcd2  12603  qredeu  12605  rpdvds  12607  isprm3  12626  divgcdodd  12651  coprm  12652  rpexp  12661  sqrt2irr  12670  qnumcl  12696  qnumdencoprm  12701  divnumden  12704  numsq  12711  phimullem  12733  eulerthlem1  12735  prmdiveq  12744  prmdivdiv  12745  hashgcdlem  12746  odzcl  12752  reumodprminv  12762  pythagtriplem19  12791  pclemub  12796  pcprendvds  12799  pcprendvds2  12800  pcpre1  12801  pcpremul  12802  pceulem  12803  pceu  12804  pczpre  12806  pczcl  12807  pcgcd1  12837  pc2dvds  12839  pcaddlem  12848  pcmpt  12852  pockthlem  12865  prmunb  12871  4sqlem7  12893  4sqlem8  12894  4sqlem9  12895  4sqlem10  12896  4sqlem14  12913  4sqlem15  12914  4sqlem16  12915  4sqlem17  12916  4sqlem18  12917  ennnfonelemg  12960  ennnfonelemf1  12975  ctiunctlemu1st  12991  nninfdclemf  13006  nninfdclemp1  13007  mgmidcl  13397  gsumfzval  13410  gsumval2  13416  mndlid  13454  prdsmndd  13467  imasmndf1  13473  dfgrp3mlem  13617  grplactf1o  13622  prdsgrpd  13628  prdsinvgd  13629  imasgrpf1  13635  subgsubm  13719  qusgrp  13755  ghmgrp1  13768  ghmf  13770  ghmnsgpreima  13792  kerf1ghm  13797  conjsubg  13800  imasrng  13905  srgdilem  13918  srgdi  13923  srglidm  13928  ringdilem  13961  ringdi  13967  ringlidm  13972  imasring  14013  imasringf1  14014  dvdsrcld  14046  unitcld  14057  unitmulcl  14062  unitnegcl  14079  rhmghm  14111  elrhmunit  14126  subrgss  14171  subrgrcl  14175  lmodvscl  14254  lmodvsdi  14260  lmodvsdir  14261  lsslsp  14378  qusring  14476  crngridl  14479  znunit  14608  znrrg  14609  psrbaglesuppg  14621  psrelbas  14624  psraddcl  14629  mplrcl  14643  uniopn  14660  restbasg  14827  cntop1  14860  cnf  14863  cnpf2  14866  lmtopcnp  14909  psmetdmdm  14983  psmetf  14984  psmet0  14986  xmetf  15009  metf  15010  blhalf  15067  xmetxpbl  15167  ioo2bl  15210  tgioo  15213  cncff  15236  rescncf  15240  cdivcncfap  15263  cnopnap  15270  divcncfap  15273  dedekindeulemeu  15281  dedekindicclemeu  15290  ivthinclemlm  15293  ivthinclemlopn  15295  ivthinclemuopn  15297  ivthinclemdisj  15299  ivthdec  15303  ivthreinc  15304  limcimolemlt  15323  limcimo  15324  limccnpcntop  15334  limccnp2lem  15335  limccnp2cntop  15336  limccoap  15337  eldvap  15341  dvbsssg  15345  dvfgg  15347  dvaddxxbr  15360  dvmulxxbr  15361  dvcoapbr  15366  dvcj  15368  dvfre  15369  dvrecap  15372  plyco  15418  plycj  15420  sin0pilem1  15440  sin0pilem2  15441  pilem3  15442  tanrpcl  15496  tangtx  15497  perfect  15660  lgsne0  15702  lgseisen  15738  lgsquad2lem2  15746  2sqlem8a  15786  2sqlem8  15787  structgrssvtx  15828  edguhgr  15920  umgrpredgv  15930  umgrnloop2  15934  umgr2edg  15990  nninfalllem1  16305  iooref1o  16333  alsi1d  16380  alsc1d  16382