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  1024  eldifad  3225  unssad  3400  opth1  4357  opth  4358  0nelop  4369  epelg  4416  poirr  4433  brrelex1  4794  brrelex  4795  asymref  5153  soirri  5162  sotri  5163  ffdmd  5539  fcnvres  5555  fun11iun  5640  funopsn  5865  elmpocl1  6258  f1od  6266  f1o2d  6268  oprssdmm  6378  elmpom  6447  fczsupp0  6472  smoiso  6546  tfrlem1  6552  swoer  6808  ecopovtrn  6879  ecopovtrng  6882  elmapssres  6920  pmresg  6923  mapsspm  6929  en1uniel  7057  pw2f1odc  7101  xpf1o  7110  sbthlemi9  7248  fsuppfund  7260  supelti  7306  supsnti  7309  supisoti  7314  ctssdccl  7415  ctfoex  7422  fodjum  7450  en2eleq  7511  djuen  7531  pw1if  7548  dftap2  7581  2omotaplemst  7588  exmidapne  7590  ccfunen  7594  dfplpq2  7685  ltbtwnnqq  7746  enq0tr  7765  elnp1st2nd  7807  prcdnql  7815  prnminu  7820  prloc  7822  genpcdl  7850  addnqprulem  7859  addlocprlemlt  7862  addlocprlemgt  7865  addlocprlem  7866  addlocpr  7867  nqprxx  7877  ltnqex  7880  addnqprlemfl  7890  addnqprlemfu  7891  appdivnq  7894  prmuloclemcalc  7896  prmuloc  7897  mullocprlem  7901  mulnqprlemfl  7906  mulnqprlemfu  7907  ltprordil  7920  ltnqpri  7925  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  ltexpri  7944  lteupri  7948  ltaprlem  7949  recexprlemell  7953  recexprlemelu  7954  recexprlemloc  7962  recexprlempr  7963  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1u  7967  aptipr  7972  cauappcvgprlemm  7976  cauappcvgprlemlol  7978  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlem1  7990  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemlol  8001  caucvgprlemladdfu  8008  caucvgprprlemloccalc  8015  caucvgprprlemnkltj  8020  caucvgprprlemnbj  8024  caucvgprprlemml  8025  caucvgprprlemlol  8029  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  suplocexprlemss  8046  suplocexprlemru  8050  suplocexprlemlub  8055  ltsrprg  8078  caucvgsrlemasr  8121  suplocsrlemb  8137  suplocsrlem  8139  suplocsr  8140  axcaucvglemcau  8229  axpre-suploclemres  8232  negf1o  8672  apreap  8878  apreim  8894  msqge0  8907  mulge0  8910  apti  8913  apsscn  8938  mulap0bad  8950  divadddivap  9018  recnz  9689  lbzbi  9966  xadd4d  10237  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccss2  10296  iccssioo2  10298  iccssico2  10299  iccen  10359  elfzole1  10512  infssfzcldc  10618  infssfzledc  10619  ioom  10644  elicore  10650  flqle  10662  flqltnz  10671  addmodlteq  10784  expclzap  10950  hashennnuni  11167  zfz1isolem1  11237  hashdmprop2dom  11241  swrdsbslen  11383  ccatswrd  11387  ccatpfx  11418  recl  11563  cvg1nlemcau  11694  cvg1nlemres  11695  resqrtth  11741  fimaxre2  11937  climcl  11992  reccn2ap  12023  nnf1o  12087  summodclem3  12091  sumpr  12124  fsump1i  12144  fisumcom2  12149  fsum00  12173  fsumparts  12181  mertenslemi1  12246  prodmodclem3  12286  fprodcom2fi  12337  addsin  12453  subsin  12454  addcos  12457  subcos  12458  sinbnd2  12465  cosbnd2  12466  sin01gt0  12473  cos01gt0  12474  divgcdz  12692  divgcdnn  12696  gcdaddm  12705  bezoutlemstep  12718  dvdsgcdb  12734  dfgcd2  12735  mulgcd  12737  gcdzeq  12743  dvdsmulgcd  12746  sqgcd  12750  bezoutr  12753  lcmval  12785  lcmcllem  12789  gcddvdslcm  12795  lcmgcdlem  12799  lcmgcd  12800  lcmgcdeq  12805  lcmdvdsb  12806  mulgcddvds  12816  rpmulgcd2  12817  qredeu  12819  rpdvds  12821  isprm3  12840  divgcdodd  12865  coprm  12866  rpexp  12875  sqrt2irr  12884  qnumcl  12910  qnumdencoprm  12915  divnumden  12918  numsq  12925  phimullem  12947  eulerthlem1  12949  prmdiveq  12958  prmdivdiv  12959  hashgcdlem  12960  odzcl  12966  reumodprminv  12976  pythagtriplem19  13005  pclemub  13010  pcprendvds  13013  pcprendvds2  13014  pcpre1  13015  pcpremul  13016  pceulem  13017  pceu  13018  pczpre  13020  pczcl  13021  pcgcd1  13051  pc2dvds  13053  pcaddlem  13062  pcmpt  13066  pockthlem  13079  prmunb  13085  4sqlem7  13107  4sqlem8  13108  4sqlem9  13109  4sqlem10  13110  4sqlem14  13127  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  4sqlem18  13131  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemimin  13193  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsv  13197  ballotfilemsgt1  13198  ballotfilemsdom  13199  ballotfilemsel1i  13200  ballotfilemsf1o  13201  ballotfilemsi  13202  ballotfilemsima  13203  ballotfilemscr  13206  ballotfilemrv  13207  ballotfilemrv2  13209  ballotfilemro  13210  ballotfilemfrc  13214  ballotfilemfrci  13215  ballotfilemfrceq  13216  ballotfilemfrcn0  13217  ballotfilemrc  13218  ballotfilemirc  13219  ballotfilemrinv0  13220  ballotfilem1ri  13222  ennnfonelemg  13238  ennnfonelemf1  13253  ctiunctlemu1st  13269  nninfdclemf  13284  nninfdclemp1  13285  mgmidcl  13675  gsumfzval  13688  gsumval2  13694  mndlid  13732  prdsmndd  13745  imasmndf1  13751  dfgrp3mlem  13895  grplactf1o  13900  prdsgrpd  13906  prdsinvgd  13907  imasgrpf1  13913  subgsubm  13997  qusgrp  14033  ghmgrp1  14046  ghmf  14048  ghmnsgpreima  14070  kerf1ghm  14075  conjsubg  14078  gsumsplit0  14147  imasrng  14184  srgdilem  14197  srgdi  14202  srglidm  14207  ringdilem  14240  ringdi  14246  ringlidm  14251  imasring  14292  imasringf1  14293  dvdsrcld  14327  unitcld  14338  unitmulcl  14343  unitnegcl  14360  rhmghm  14392  elrhmunit  14407  subrgss  14453  subrgrcl  14457  rrgsupp  14497  lmodvscl  14565  lmodvsdi  14571  lmodvsdir  14572  lsslsp  14689  qusring  14787  crngridl  14790  znunit  14919  znrrg  14920  psrbaglesuppg  14933  psrbagcon  14938  psrbagconcl  14939  psrelbas  14942  psraddcl  14947  mplrcl  14961  uniopn  14978  restbasg  15145  cntop1  15178  cnf  15181  cnpf2  15184  lmtopcnp  15227  psmetdmdm  15301  psmetf  15302  psmet0  15304  xmetf  15327  metf  15328  blhalf  15385  xmetxpbl  15485  ioo2bl  15528  tgioo  15531  cncff  15554  rescncf  15558  cdivcncfap  15581  cnopnap  15588  divcncfap  15591  dedekindeulemeu  15599  dedekindicclemeu  15608  ivthinclemlm  15611  ivthinclemlopn  15613  ivthinclemuopn  15615  ivthinclemdisj  15617  ivthdec  15621  ivthreinc  15622  limcimolemlt  15641  limcimo  15642  limccnpcntop  15652  limccnp2lem  15653  limccnp2cntop  15654  limccoap  15655  eldvap  15659  dvbsssg  15663  dvfgg  15665  dvaddxxbr  15678  dvmulxxbr  15679  dvcoapbr  15684  dvcj  15686  dvfre  15687  dvrecap  15690  plyco  15736  plycj  15738  sin0pilem1  15758  sin0pilem2  15759  pilem3  15760  tanrpcl  15814  tangtx  15815  perfect  15981  lgsne0  16023  lgseisen  16059  lgsquad2lem2  16067  2sqlem8a  16107  2sqlem8  16108  structgrssvtx  16149  edguhgr  16244  umgrpredgv  16254  umgrnloop2  16258  umgr2edg  16314  subuhgr  16379  subumgr  16381  subusgr  16382  wlkpropg  16431  wlkv  16433  wlkvtxeledgg  16451  wlkvtxiedgg  16453  wlk1walkdom  16466  trlsv  16491  clwwlksswrd  16504  clwwlkclwwlkn  16516  eupthv  16553  eupthseg  16559  eupth2lem3lem3fi  16577  eupth2lem3lem4fi  16580  eupth2lemsfi  16585  eulerpathprum  16587  nninfalllem1  16898  iooref1o  16930  gfsumval  16974  alsi1d  16990  alsc1d  16992