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  4378  opth  4379  0nelop  4390  epelg  4437  poirr  4454  brrelex1  4816  brrelex  4817  asymref  5176  soirri  5185  sotri  5186  ffdmd  5562  fcnvres  5578  fun11iun  5663  funopsn  5894  elmpocl1  6288  f1od  6296  f1o2d  6298  oprssdmm  6409  elmpom  6478  fczsupp0  6503  smoiso  6577  tfrlem1  6583  swoer  6839  ecopovtrn  6910  ecopovtrng  6913  elmapssres  6958  pmresg  6961  mapsspm  6967  en1uniel  7095  pw2f1odc  7139  xpf1o  7148  sbthlemi9  7287  fsuppfund  7299  supelti  7348  supsnti  7351  supisoti  7356  ctssdccl  7457  ctfoex  7464  fodjum  7492  en2eleq  7553  djuen  7573  pw1if  7590  dftap2  7623  2omotaplemst  7630  exmidapne  7632  ccfunen  7636  dfplpq2  7727  ltbtwnnqq  7788  enq0tr  7807  elnp1st2nd  7849  prcdnql  7857  prnminu  7862  prloc  7864  genpcdl  7892  addnqprulem  7901  addlocprlemlt  7904  addlocprlemgt  7907  addlocprlem  7908  addlocpr  7909  nqprxx  7919  ltnqex  7922  addnqprlemfl  7932  addnqprlemfu  7933  appdivnq  7936  prmuloclemcalc  7938  prmuloc  7939  mullocprlem  7943  mulnqprlemfl  7948  mulnqprlemfu  7949  ltprordil  7962  ltnqpri  7967  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  ltexpri  7986  lteupri  7990  ltaprlem  7991  recexprlemell  7995  recexprlemelu  7996  recexprlemloc  8004  recexprlempr  8005  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1u  8009  aptipr  8014  cauappcvgprlemm  8018  cauappcvgprlemlol  8020  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlem1  8032  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemlol  8043  caucvgprlemladdfu  8050  caucvgprprlemloccalc  8057  caucvgprprlemnkltj  8062  caucvgprprlemnbj  8066  caucvgprprlemml  8067  caucvgprprlemlol  8071  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  suplocexprlemss  8088  suplocexprlemru  8092  suplocexprlemlub  8097  ltsrprg  8120  caucvgsrlemasr  8163  suplocsrlemb  8179  suplocsrlem  8181  suplocsr  8182  axcaucvglemcau  8271  axpre-suploclemres  8274  negf1o  8716  apreap  8923  apreim  8939  msqge0  8952  mulge0  8955  apti  8958  apsscn  8983  mulap0bad  8995  divadddivap  9065  recnz  9750  lbzbi  10032  xadd4d  10304  ixxss1  10323  ixxss2  10324  ixxss12  10325  iccss2  10363  iccssioo2  10365  iccssico2  10366  iccen  10426  elfzole1  10580  infssfzcldc  10686  infssfzledc  10687  ioom  10712  elicore  10718  flqle  10732  flapge  10737  flaplt  10739  flqltnz  10743  addmodlteq  10856  expclzap  11022  hashennnuni  11240  zfz1isolem1  11314  hashdmprop2dom  11318  swrdsbslen  11460  ccatswrd  11464  ccatpfx  11495  recl  11640  sq01  11682  cvg1nlemcau  11772  cvg1nlemres  11773  resqrtth  11819  fimaxre2  12016  climcl  12073  reccn2ap  12104  nnf1o  12168  summodclem3  12172  sumpr  12205  fsump1i  12225  fisumcom2  12230  fsum00  12254  fsumparts  12262  mertenslemi1  12327  prodmodclem3  12367  fprodcom2fi  12418  addsin  12534  subsin  12535  addcos  12538  subcos  12539  sinbnd2  12546  cosbnd2  12547  sin01gt0  12554  cos01gt0  12555  divgcdz  12773  divgcdnn  12777  gcdaddm  12786  bezoutlemstep  12799  dvdsgcdb  12815  dfgcd2  12816  mulgcd  12818  gcdzeq  12824  dvdsmulgcd  12827  sqgcd  12831  bezoutr  12834  lcmval  12866  lcmcllem  12870  gcddvdslcm  12876  lcmgcdlem  12880  lcmgcd  12881  lcmgcdeq  12886  lcmdvdsb  12887  mulgcddvds  12897  rpmulgcd2  12898  qredeu  12900  rpdvds  12902  isprm3  12921  divgcdodd  12947  coprm  12948  rpexp  12957  sqrt2irr  12966  qnumcl  12993  qnumdencoprm  12998  divnumden  13001  numsq  13008  phimullem  13032  eulerthlem1  13034  prmdiveq  13043  prmdivdiv  13044  hashgcdlem  13045  odzcl  13051  reumodprminv  13061  pythagtriplem19  13090  pclemub  13095  pcprendvds  13098  pcprendvds2  13099  pcpre1  13100  pcpremul  13101  pceulem  13102  pceu  13103  pczpre  13105  pczcl  13106  pcgcd1  13136  pc2dvds  13138  pcaddlem  13147  pcmpt  13151  pockthlem  13164  prmunb  13170  4sqlem7  13192  4sqlem8  13193  4sqlem9  13194  4sqlem10  13195  4sqlem14  13212  4sqlem15  13213  4sqlem16  13214  4sqlem17  13215  4sqlem18  13216  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemimin  13307  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemsv  13311  ballotfilemsgt1  13312  ballotfilemsdom  13313  ballotfilemsel1i  13314  ballotfilemsf1o  13315  ballotfilemsi  13316  ballotfilemsima  13317  ballotfilemscr  13320  ballotfilemrv  13321  ballotfilemrv2  13323  ballotfilemro  13324  ballotfilemfrc  13328  ballotfilemfrci  13329  ballotfilemfrceq  13330  ballotfilemfrcn0  13331  ballotfilemrc  13332  ballotfilemirc  13333  ballotfilemrinv0  13334  ballotfilem1ri  13336  ennnfonelemg  13352  ennnfonelemf1  13367  ctiunctlemu1st  13383  nninfdclemf  13398  nninfdclemp1  13399  mgmidcl  13757  gzsumfzval  13770  gzsumval2  13773  mndlid  13807  imasmndf1  13820  dfgrp3mlem  13962  grplactf1o  13967  imasgrpf1  13974  subgsubm  14058  qusgrp  14094  ghmgrp1  14107  ghmf  14109  ghmnsgpreima  14131  kerf1ghm  14136  conjsubg  14139  resscntz  14166  gzsumsplit0  14238  gsumvalfi  14242  prdsmndd  14301  prdsgrpd  14304  prdsinvgd  14305  imasrng  14362  srgdilem  14380  srgdi  14385  srglidm  14390  ringdilem  14423  ringdi  14430  ringlidm  14435  imasring  14478  imasringf1  14479  dvdsrcld  14513  unitcld  14524  unitmulcl  14529  unitnegcl  14546  rhmghm  14578  elrhmunit  14593  subrgss  14639  subrgrcl  14643  rrgsupp  14683  lmodvscl  14750  lmodvsdi  14757  lmodvsdir  14758  lsslsp  14875  qusring  14973  crngridl  14976  znunit  15103  znrrg  15104  assaass  15113  assalmod  15115  psrbaglesuppg  15166  psrbagcon  15171  psrbagconcl  15173  gsumbagdiaglem  15175  gsumbagdiagfi  15176  psrass1filem  15177  psrelbas  15179  psraddcl  15184  rhmpsrfilem2  15185  psrmulfval  15187  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  mplrcl  15210  uniopn  15227  restbasg  15394  cntop1  15427  cnf  15430  cnpf2  15433  lmtopcnp  15476  psmetdmdm  15550  psmetf  15551  psmet0  15553  xmetf  15576  metf  15577  blhalf  15634  xmetxpbl  15734  ioo2bl  15777  tgioo  15780  cncff  15803  rescncf  15807  cdivcncfap  15830  cnopnap  15837  divcncfap  15840  dedekindeulemeu  15848  dedekindicclemeu  15857  ivthinclemlm  15860  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthinclemdisj  15866  ivthdec  15870  ivthreinc  15871  limcimolemlt  15890  limcimo  15891  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  limccoap  15904  eldvap  15908  dvbsssg  15912  dvfgg  15914  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcj  15935  dvfre  15936  dvrecap  15939  plyco  15985  plycj  15987  sin0pilem1  16008  sin0pilem2  16009  pilem3  16010  tanrpcl  16064  tangtx  16065  zprmlogbaplem2  16216  zprmlogbaplem3  16217  ppiqsval2  16241  chtqge0  16247  chtqwordi  16263  chtublem  16295  perfect  16301  bposlem1  16311  bposlem4  16314  bposlem5  16315  bposlem9  16319  lgsne0  16362  lgseisen  16398  lgsquad2lem2  16406  2sqlem8a  16446  2sqlem8  16447  structgrssvtx  16488  edguhgr  16583  umgrpredgv  16593  umgrnloop2  16597  umgr2edg  16653  subuhgr  16718  subumgr  16720  subusgr  16721  wlkpropg  16770  wlkv  16772  wlkvtxeledgg  16790  wlkvtxiedgg  16792  wlk1walkdom  16805  trlsv  16830  clwwlksswrd  16843  clwwlkclwwlkn  16855  eupthv  16892  eupthseg  16898  eupth2lem3lem3fi  16916  eupth2lem3lem4fi  16919  eupth2lemsfi  16924  eulerpathprum  16926  nninfalllem1  17257  iooref1o  17289  als1d  17340  rals1d  17342  alseu1d  17376  ralseu1d  17378