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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is used by:  biimp  118  simplbi  274  simprbda  383  simplld  532  simplrd  534  simprld  536  simp1  1028  eldifad  3231  unssad  3406  opth1  4376  opth  4377  0nelop  4388  epelg  4435  poirr  4452  brrelex1  4814  brrelex  4815  asymref  5173  soirri  5182  sotri  5183  ffdmd  5559  fcnvres  5575  fun11iun  5660  funopsn  5891  elmpocl1  6285  f1od  6293  f1o2d  6295  oprssdmm  6405  elmpom  6474  fczsupp0  6499  smoiso  6573  tfrlem1  6579  swoer  6835  ecopovtrn  6906  ecopovtrng  6909  elmapssres  6954  pmresg  6957  mapsspm  6963  en1uniel  7091  pw2f1odc  7135  xpf1o  7144  sbthlemi9  7282  fsuppfund  7294  supelti  7343  supsnti  7346  supisoti  7351  ctssdccl  7452  ctfoex  7459  fodjum  7487  en2eleq  7548  djuen  7568  pw1if  7585  dftap2  7618  2omotaplemst  7625  exmidapne  7627  ccfunen  7631  dfplpq2  7722  ltbtwnnqq  7783  enq0tr  7802  elnp1st2nd  7844  prcdnql  7852  prnminu  7857  prloc  7859  genpcdl  7887  addnqprulem  7896  addlocprlemlt  7899  addlocprlemgt  7902  addlocprlem  7903  addlocpr  7904  nqprxx  7914  ltnqex  7917  addnqprlemfl  7927  addnqprlemfu  7928  appdivnq  7931  prmuloclemcalc  7933  prmuloc  7934  mullocprlem  7938  mulnqprlemfl  7943  mulnqprlemfu  7944  ltprordil  7957  ltnqpri  7962  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltexpri  7981  lteupri  7985  ltaprlem  7986  recexprlemell  7990  recexprlemelu  7991  recexprlemloc  7999  recexprlempr  8000  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1u  8004  aptipr  8009  cauappcvgprlemm  8013  cauappcvgprlemlol  8015  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlem1  8027  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemlol  8038  caucvgprlemladdfu  8045  caucvgprprlemloccalc  8052  caucvgprprlemnkltj  8057  caucvgprprlemnbj  8061  caucvgprprlemml  8062  caucvgprprlemlol  8066  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  suplocexprlemss  8083  suplocexprlemru  8087  suplocexprlemlub  8092  ltsrprg  8115  caucvgsrlemasr  8158  suplocsrlemb  8174  suplocsrlem  8176  suplocsr  8177  axcaucvglemcau  8266  axpre-suploclemres  8269  negf1o  8711  apreap  8918  apreim  8934  msqge0  8947  mulge0  8950  apti  8953  apsscn  8978  mulap0bad  8990  divadddivap  9060  recnz  9744  lbzbi  10026  xadd4d  10298  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iccssioo2  10359  iccssico2  10360  iccen  10420  elfzole1  10574  infssfzcldc  10680  infssfzledc  10681  ioom  10706  elicore  10712  flqle  10726  flapge  10731  flqltnz  10736  addmodlteq  10849  expclzap  11015  hashennnuni  11233  zfz1isolem1  11307  hashdmprop2dom  11311  swrdsbslen  11453  ccatswrd  11457  ccatpfx  11488  recl  11633  sq01  11675  cvg1nlemcau  11765  cvg1nlemres  11766  resqrtth  11812  fimaxre2  12009  climcl  12066  reccn2ap  12097  nnf1o  12161  summodclem3  12165  sumpr  12198  fsump1i  12218  fisumcom2  12223  fsum00  12247  fsumparts  12255  mertenslemi1  12320  prodmodclem3  12360  fprodcom2fi  12411  addsin  12527  subsin  12528  addcos  12531  subcos  12532  sinbnd2  12539  cosbnd2  12540  sin01gt0  12547  cos01gt0  12548  divgcdz  12766  divgcdnn  12770  gcdaddm  12779  bezoutlemstep  12792  dvdsgcdb  12808  dfgcd2  12809  mulgcd  12811  gcdzeq  12817  dvdsmulgcd  12820  sqgcd  12824  bezoutr  12827  lcmval  12859  lcmcllem  12863  gcddvdslcm  12869  lcmgcdlem  12873  lcmgcd  12874  lcmgcdeq  12879  lcmdvdsb  12880  mulgcddvds  12890  rpmulgcd2  12891  qredeu  12893  rpdvds  12895  isprm3  12914  divgcdodd  12940  coprm  12941  rpexp  12950  sqrt2irr  12959  qnumcl  12986  qnumdencoprm  12991  divnumden  12994  numsq  13001  phimullem  13025  eulerthlem1  13027  prmdiveq  13036  prmdivdiv  13037  hashgcdlem  13038  odzcl  13044  reumodprminv  13054  pythagtriplem19  13083  pclemub  13088  pcprendvds  13091  pcprendvds2  13092  pcpre1  13093  pcpremul  13094  pceulem  13095  pceu  13096  pczpre  13098  pczcl  13099  pcgcd1  13129  pc2dvds  13131  pcaddlem  13140  pcmpt  13144  pockthlem  13157  prmunb  13163  4sqlem7  13185  4sqlem8  13186  4sqlem9  13187  4sqlem10  13188  4sqlem14  13205  4sqlem15  13206  4sqlem16  13207  4sqlem17  13208  4sqlem18  13209  ballotfilem2  13279  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilem4  13292  ballotfilemi1  13296  ballotfilemimin  13300  ballotfilemic  13301  ballotfilem1c  13302  ballotfilemsv  13304  ballotfilemsgt1  13305  ballotfilemsdom  13306  ballotfilemsel1i  13307  ballotfilemsf1o  13308  ballotfilemsi  13309  ballotfilemsima  13310  ballotfilemscr  13313  ballotfilemrv  13314  ballotfilemrv2  13316  ballotfilemro  13317  ballotfilemfrc  13321  ballotfilemfrci  13322  ballotfilemfrceq  13323  ballotfilemfrcn0  13324  ballotfilemrc  13325  ballotfilemirc  13326  ballotfilemrinv0  13327  ballotfilem1ri  13329  ennnfonelemg  13345  ennnfonelemf1  13360  ctiunctlemu1st  13376  nninfdclemf  13391  nninfdclemp1  13392  mgmidcl  13749  gzsumfzval  13762  gzsumval2  13765  mndlid  13799  imasmndf1  13812  dfgrp3mlem  13954  grplactf1o  13959  imasgrpf1  13966  subgsubm  14050  qusgrp  14086  ghmgrp1  14099  ghmf  14101  ghmnsgpreima  14123  kerf1ghm  14128  conjsubg  14131  gzsumsplit0  14199  gsumvalfi  14203  prdsmndd  14245  prdsgrpd  14248  prdsinvgd  14249  imasrng  14306  srgdilem  14324  srgdi  14329  srglidm  14334  ringdilem  14367  ringdi  14374  ringlidm  14379  imasring  14420  imasringf1  14421  dvdsrcld  14455  unitcld  14466  unitmulcl  14471  unitnegcl  14488  rhmghm  14520  elrhmunit  14535  subrgss  14581  subrgrcl  14585  rrgsupp  14625  lmodvscl  14692  lmodvsdi  14699  lmodvsdir  14700  lsslsp  14817  qusring  14915  crngridl  14918  znunit  15045  znrrg  15046  assaass  15055  assalmod  15057  psrbaglesuppg  15108  psrbagcon  15113  psrbagconcl  15115  psrelbas  15118  psraddcl  15123  mplrcl  15137  uniopn  15154  restbasg  15321  cntop1  15354  cnf  15357  cnpf2  15360  lmtopcnp  15403  psmetdmdm  15477  psmetf  15478  psmet0  15480  xmetf  15503  metf  15504  blhalf  15561  xmetxpbl  15661  ioo2bl  15704  tgioo  15707  cncff  15730  rescncf  15734  cdivcncfap  15757  cnopnap  15764  divcncfap  15767  dedekindeulemeu  15775  dedekindicclemeu  15784  ivthinclemlm  15787  ivthinclemlopn  15789  ivthinclemuopn  15791  ivthinclemdisj  15793  ivthdec  15797  ivthreinc  15798  limcimolemlt  15817  limcimo  15818  limccnpcntop  15828  limccnp2lem  15829  limccnp2cntop  15830  limccoap  15831  eldvap  15835  dvbsssg  15839  dvfgg  15841  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  dvcj  15862  dvfre  15863  dvrecap  15866  plyco  15912  plycj  15914  sin0pilem1  15935  sin0pilem2  15936  pilem3  15937  tanrpcl  15991  tangtx  15992  zprmlogbaplem2  16138  zprmlogbaplem3  16139  ppiqsval2  16163  chtqge0  16169  chtqwordi  16185  chtublem  16217  perfect  16223  bposlem1  16233  bposlem4  16236  bposlem5  16237  lgsne0  16279  lgseisen  16315  lgsquad2lem2  16323  2sqlem8a  16363  2sqlem8  16364  structgrssvtx  16405  edguhgr  16500  umgrpredgv  16510  umgrnloop2  16514  umgr2edg  16570  subuhgr  16635  subumgr  16637  subusgr  16638  wlkpropg  16687  wlkv  16689  wlkvtxeledgg  16707  wlkvtxiedgg  16709  wlk1walkdom  16722  trlsv  16747  clwwlksswrd  16760  clwwlkclwwlkn  16772  eupthv  16809  eupthseg  16815  eupth2lem3lem3fi  16833  eupth2lem3lem4fi  16836  eupth2lemsfi  16841  eulerpathprum  16843  nninfalllem1  17173  iooref1o  17205  als1d  17255  rals1d  17257  alseu1d  17291  ralseu1d  17293