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  8673  apreap  8879  apreim  8895  msqge0  8908  mulge0  8911  apti  8914  apsscn  8939  mulap0bad  8951  divadddivap  9021  recnz  9692  lbzbi  9969  xadd4d  10240  ixxss1  10259  ixxss2  10260  ixxss12  10261  iccss2  10299  iccssioo2  10301  iccssico2  10302  iccen  10362  elfzole1  10515  infssfzcldc  10621  infssfzledc  10622  ioom  10647  elicore  10653  flqle  10665  flqltnz  10674  addmodlteq  10787  expclzap  10953  hashennnuni  11170  zfz1isolem1  11240  hashdmprop2dom  11244  swrdsbslen  11386  ccatswrd  11390  ccatpfx  11421  recl  11566  sq01  11608  cvg1nlemcau  11698  cvg1nlemres  11699  resqrtth  11745  fimaxre2  11941  climcl  11996  reccn2ap  12027  nnf1o  12091  summodclem3  12095  sumpr  12128  fsump1i  12148  fisumcom2  12153  fsum00  12177  fsumparts  12185  mertenslemi1  12250  prodmodclem3  12290  fprodcom2fi  12341  addsin  12457  subsin  12458  addcos  12461  subcos  12462  sinbnd2  12469  cosbnd2  12470  sin01gt0  12477  cos01gt0  12478  divgcdz  12696  divgcdnn  12700  gcdaddm  12709  bezoutlemstep  12722  dvdsgcdb  12738  dfgcd2  12739  mulgcd  12741  gcdzeq  12747  dvdsmulgcd  12750  sqgcd  12754  bezoutr  12757  lcmval  12789  lcmcllem  12793  gcddvdslcm  12799  lcmgcdlem  12803  lcmgcd  12804  lcmgcdeq  12809  lcmdvdsb  12810  mulgcddvds  12820  rpmulgcd2  12821  qredeu  12823  rpdvds  12825  isprm3  12844  divgcdodd  12869  coprm  12870  rpexp  12879  sqrt2irr  12888  qnumcl  12914  qnumdencoprm  12919  divnumden  12922  numsq  12929  phimullem  12951  eulerthlem1  12953  prmdiveq  12962  prmdivdiv  12963  hashgcdlem  12964  odzcl  12970  reumodprminv  12980  pythagtriplem19  13009  pclemub  13014  pcprendvds  13017  pcprendvds2  13018  pcpre1  13019  pcpremul  13020  pceulem  13021  pceu  13022  pczpre  13024  pczcl  13025  pcgcd1  13055  pc2dvds  13057  pcaddlem  13066  pcmpt  13070  pockthlem  13083  prmunb  13089  4sqlem7  13111  4sqlem8  13112  4sqlem9  13113  4sqlem10  13114  4sqlem14  13131  4sqlem15  13132  4sqlem16  13133  4sqlem17  13134  4sqlem18  13135  ballotfilem2  13176  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilem4  13189  ballotfilemi1  13193  ballotfilemimin  13197  ballotfilemic  13198  ballotfilem1c  13199  ballotfilemsv  13201  ballotfilemsgt1  13202  ballotfilemsdom  13203  ballotfilemsel1i  13204  ballotfilemsf1o  13205  ballotfilemsi  13206  ballotfilemsima  13207  ballotfilemscr  13210  ballotfilemrv  13211  ballotfilemrv2  13213  ballotfilemro  13214  ballotfilemfrc  13218  ballotfilemfrci  13219  ballotfilemfrceq  13220  ballotfilemfrcn0  13221  ballotfilemrc  13222  ballotfilemirc  13223  ballotfilemrinv0  13224  ballotfilem1ri  13226  ennnfonelemg  13242  ennnfonelemf1  13257  ctiunctlemu1st  13273  nninfdclemf  13288  nninfdclemp1  13289  mgmidcl  13645  gsumfzval  13658  gsumval2  13664  mndlid  13700  imasmndf1  13713  dfgrp3mlem  13857  grplactf1o  13862  imasgrpf1  13869  subgsubm  13953  qusgrp  13989  ghmgrp1  14002  ghmf  14004  ghmnsgpreima  14026  kerf1ghm  14031  conjsubg  14034  gsumsplit0  14103  gfsumval  14106  prdsmndd  14140  prdsgrpd  14143  prdsinvgd  14144  imasrng  14199  srgdilem  14216  srgdi  14221  srglidm  14226  ringdilem  14259  ringdi  14265  ringlidm  14270  imasring  14311  imasringf1  14312  dvdsrcld  14346  unitcld  14357  unitmulcl  14362  unitnegcl  14379  rhmghm  14411  elrhmunit  14426  subrgss  14472  subrgrcl  14476  rrgsupp  14516  lmodvscl  14583  lmodvsdi  14589  lmodvsdir  14590  lsslsp  14707  qusring  14805  crngridl  14808  znunit  14937  znrrg  14938  psrbaglesuppg  14951  psrbagcon  14956  psrbagconcl  14957  psrelbas  14960  psraddcl  14965  mplrcl  14979  uniopn  14996  restbasg  15163  cntop1  15196  cnf  15199  cnpf2  15202  lmtopcnp  15245  psmetdmdm  15319  psmetf  15320  psmet0  15322  xmetf  15345  metf  15346  blhalf  15403  xmetxpbl  15503  ioo2bl  15546  tgioo  15549  cncff  15572  rescncf  15576  cdivcncfap  15599  cnopnap  15606  divcncfap  15609  dedekindeulemeu  15617  dedekindicclemeu  15626  ivthinclemlm  15629  ivthinclemlopn  15631  ivthinclemuopn  15633  ivthinclemdisj  15635  ivthdec  15639  ivthreinc  15640  limcimolemlt  15659  limcimo  15660  limccnpcntop  15670  limccnp2lem  15671  limccnp2cntop  15672  limccoap  15673  eldvap  15677  dvbsssg  15681  dvfgg  15683  dvaddxxbr  15696  dvmulxxbr  15697  dvcoapbr  15702  dvcj  15704  dvfre  15705  dvrecap  15708  plyco  15754  plycj  15756  sin0pilem1  15776  sin0pilem2  15777  pilem3  15778  tanrpcl  15832  tangtx  15833  perfect  15999  lgsne0  16041  lgseisen  16077  lgsquad2lem2  16085  2sqlem8a  16125  2sqlem8  16126  structgrssvtx  16167  edguhgr  16262  umgrpredgv  16272  umgrnloop2  16276  umgr2edg  16332  subuhgr  16397  subumgr  16399  subusgr  16400  wlkpropg  16449  wlkv  16451  wlkvtxeledgg  16469  wlkvtxiedgg  16471  wlk1walkdom  16484  trlsv  16509  clwwlksswrd  16522  clwwlkclwwlkn  16534  eupthv  16571  eupthseg  16577  eupth2lem3lem3fi  16595  eupth2lem3lem4fi  16598  eupth2lemsfi  16603  eulerpathprum  16605  nninfalllem1  16926  iooref1o  16958  alsi1d  17006  alsc1d  17008