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  1000  eldifad  3179  unssad  3352  opth1  4285  opth  4286  0nelop  4297  epelg  4342  poirr  4359  brrelex1  4719  brrelex  4720  asymref  5074  soirri  5083  sotri  5084  ffdmd  5454  fcnvres  5468  fun11iun  5552  funopsn  5772  elmpocl1  6152  f1od  6159  f1o2d  6161  oprssdmm  6267  smoiso  6398  tfrlem1  6404  swoer  6658  ecopovtrn  6729  ecopovtrng  6732  elmapssres  6770  pmresg  6773  mapsspm  6779  en1uniel  6906  pw2f1odc  6944  xpf1o  6953  sbthlemi9  7079  supelti  7116  supsnti  7119  supisoti  7124  ctssdccl  7225  ctfoex  7232  fodjum  7260  en2eleq  7316  djuen  7336  dftap2  7376  2omotaplemst  7383  exmidapne  7385  ccfunen  7389  dfplpq2  7480  ltbtwnnqq  7541  enq0tr  7560  elnp1st2nd  7602  prcdnql  7610  prnminu  7615  prloc  7617  genpcdl  7645  addnqprulem  7654  addlocprlemlt  7657  addlocprlemgt  7660  addlocprlem  7661  addlocpr  7662  nqprxx  7672  ltnqex  7675  addnqprlemfl  7685  addnqprlemfu  7686  appdivnq  7689  prmuloclemcalc  7691  prmuloc  7692  mullocprlem  7696  mulnqprlemfl  7701  mulnqprlemfu  7702  ltprordil  7715  ltnqpri  7720  ltexprlemm  7726  ltexprlemopl  7727  ltexprlemlol  7728  ltexprlemopu  7729  ltexprlemupu  7730  ltexprlemdisj  7732  ltexprlemloc  7733  ltexprlemfl  7735  ltexprlemrl  7736  ltexprlemfu  7737  ltexprlemru  7738  ltexpri  7739  lteupri  7743  ltaprlem  7744  recexprlemell  7748  recexprlemelu  7749  recexprlemloc  7757  recexprlempr  7758  recexprlem1ssl  7759  recexprlem1ssu  7760  recexprlemss1u  7762  aptipr  7767  cauappcvgprlemm  7771  cauappcvgprlemlol  7773  cauappcvgprlemladdfu  7780  cauappcvgprlemladdfl  7781  cauappcvgprlemladdru  7782  cauappcvgprlem1  7785  caucvgprlemnkj  7792  caucvgprlemnbj  7793  caucvgprlemm  7794  caucvgprlemlol  7796  caucvgprlemladdfu  7803  caucvgprprlemloccalc  7810  caucvgprprlemnkltj  7815  caucvgprprlemnbj  7819  caucvgprprlemml  7820  caucvgprprlemlol  7824  caucvgprprlemloc  7829  caucvgprprlemexbt  7832  suplocexprlemss  7841  suplocexprlemru  7845  suplocexprlemlub  7850  ltsrprg  7873  caucvgsrlemasr  7916  suplocsrlemb  7932  suplocsrlem  7934  suplocsr  7935  axcaucvglemcau  8024  axpre-suploclemres  8027  negf1o  8467  apreap  8673  apreim  8689  msqge0  8702  mulge0  8705  apti  8708  apsscn  8733  mulap0bad  8745  divadddivap  8813  recnz  9479  lbzbi  9750  xadd4d  10020  ixxss1  10039  ixxss2  10040  ixxss12  10041  iccss2  10079  iccssioo2  10081  iccssico2  10082  iccen  10141  elfzole1  10291  ioom  10416  elicore  10422  flqle  10434  flqltnz  10443  addmodlteq  10556  expclzap  10722  hashennnuni  10937  zfz1isolem1  10998  hashdmprop2dom  11002  swrdsbslen  11133  ccatswrd  11137  ccatpfx  11166  recl  11214  cvg1nlemcau  11345  cvg1nlemres  11346  resqrtth  11392  fimaxre2  11588  climcl  11643  reccn2ap  11674  nnf1o  11737  summodclem3  11741  sumpr  11774  fsump1i  11794  fisumcom2  11799  fsum00  11823  fsumparts  11831  mertenslemi1  11896  prodmodclem3  11936  fprodcom2fi  11987  addsin  12103  subsin  12104  addcos  12107  subcos  12108  sinbnd2  12115  cosbnd2  12116  sin01gt0  12123  cos01gt0  12124  divgcdz  12342  divgcdnn  12346  gcdaddm  12355  bezoutlemstep  12368  dvdsgcdb  12384  dfgcd2  12385  mulgcd  12387  gcdzeq  12393  dvdsmulgcd  12396  sqgcd  12400  bezoutr  12403  lcmval  12435  lcmcllem  12439  gcddvdslcm  12445  lcmgcdlem  12449  lcmgcd  12450  lcmgcdeq  12455  lcmdvdsb  12456  mulgcddvds  12466  rpmulgcd2  12467  qredeu  12469  rpdvds  12471  isprm3  12490  divgcdodd  12515  coprm  12516  rpexp  12525  sqrt2irr  12534  qnumcl  12560  qnumdencoprm  12565  divnumden  12568  numsq  12575  phimullem  12597  eulerthlem1  12599  prmdiveq  12608  prmdivdiv  12609  hashgcdlem  12610  odzcl  12616  reumodprminv  12626  pythagtriplem19  12655  pclemub  12660  pcprendvds  12663  pcprendvds2  12664  pcpre1  12665  pcpremul  12666  pceulem  12667  pceu  12668  pczpre  12670  pczcl  12671  pcgcd1  12701  pc2dvds  12703  pcaddlem  12712  pcmpt  12716  pockthlem  12729  prmunb  12735  4sqlem7  12757  4sqlem8  12758  4sqlem9  12759  4sqlem10  12760  4sqlem14  12777  4sqlem15  12778  4sqlem16  12779  4sqlem17  12780  4sqlem18  12781  ennnfonelemg  12824  ennnfonelemf1  12839  ctiunctlemu1st  12855  nninfdclemf  12870  nninfdclemp1  12871  mgmidcl  13260  gsumfzval  13273  gsumval2  13279  mndlid  13317  prdsmndd  13330  imasmndf1  13336  dfgrp3mlem  13480  grplactf1o  13485  prdsgrpd  13491  prdsinvgd  13492  imasgrpf1  13498  subgsubm  13582  qusgrp  13618  ghmgrp1  13631  ghmf  13633  ghmnsgpreima  13655  kerf1ghm  13660  conjsubg  13663  imasrng  13768  srgdilem  13781  srgdi  13786  srglidm  13791  ringdilem  13824  ringdi  13830  ringlidm  13835  imasring  13876  imasringf1  13877  dvdsrcld  13909  unitcld  13920  unitmulcl  13925  unitnegcl  13942  rhmghm  13974  elrhmunit  13989  subrgss  14034  subrgrcl  14038  lmodvscl  14117  lmodvsdi  14123  lmodvsdir  14124  lsslsp  14241  qusring  14339  crngridl  14342  znunit  14471  znrrg  14472  psrbaglesuppg  14484  psrelbas  14487  psraddcl  14492  mplrcl  14506  uniopn  14523  restbasg  14690  cntop1  14723  cnf  14726  cnpf2  14729  lmtopcnp  14772  psmetdmdm  14846  psmetf  14847  psmet0  14849  xmetf  14872  metf  14873  blhalf  14930  xmetxpbl  15030  ioo2bl  15073  tgioo  15076  cncff  15099  rescncf  15103  cdivcncfap  15126  cnopnap  15133  divcncfap  15136  dedekindeulemeu  15144  dedekindicclemeu  15153  ivthinclemlm  15156  ivthinclemlopn  15158  ivthinclemuopn  15160  ivthinclemdisj  15162  ivthdec  15166  ivthreinc  15167  limcimolemlt  15186  limcimo  15187  limccnpcntop  15197  limccnp2lem  15198  limccnp2cntop  15199  limccoap  15200  eldvap  15204  dvbsssg  15208  dvfgg  15210  dvaddxxbr  15223  dvmulxxbr  15224  dvcoapbr  15229  dvcj  15231  dvfre  15232  dvrecap  15235  plyco  15281  plycj  15283  sin0pilem1  15303  sin0pilem2  15304  pilem3  15305  tanrpcl  15359  tangtx  15360  perfect  15523  lgsne0  15565  lgseisen  15601  lgsquad2lem2  15609  2sqlem8a  15649  2sqlem8  15650  structgrssvtx  15691  nninfalllem1  16060  iooref1o  16088  alsi1d  16135  alsc1d  16137