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  6578  tfrlem1  6584  swoer  6840  ecopovtrn  6911  ecopovtrng  6914  elmapssres  6959  pmresg  6962  mapsspm  6968  en1uniel  7097  pw2f1odc  7141  xpf1o  7150  sbthlemi9  7289  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  9749  lbzbi  10031  xadd4d  10303  ixxss1  10322  ixxss2  10323  ixxss12  10324  iccss2  10362  iccssioo2  10364  iccssico2  10365  iccen  10425  elfzole1  10579  infssfzcldc  10685  infssfzledc  10686  ioom  10711  elicore  10717  flqle  10731  flapge  10736  flaplt  10738  flqltnz  10742  addmodlteq  10855  expclzap  11021  hashennnuni  11239  zfz1isolem1  11313  hashdmprop2dom  11317  swrdsbslen  11459  ccatswrd  11463  ccatpfx  11494  recl  11639  sq01  11681  cvg1nlemcau  11771  cvg1nlemres  11772  resqrtth  11818  fimaxre2  12015  climcl  12072  reccn2ap  12103  nnf1o  12167  summodclem3  12171  sumpr  12204  fsump1i  12224  fisumcom2  12229  fsum00  12253  fsumparts  12261  mertenslemi1  12326  prodmodclem3  12366  fprodcom2fi  12417  addsin  12533  subsin  12534  addcos  12537  subcos  12538  sinbnd2  12545  cosbnd2  12546  sin01gt0  12553  cos01gt0  12554  divgcdz  12772  divgcdnn  12776  gcdaddm  12785  bezoutlemstep  12798  dvdsgcdb  12814  dfgcd2  12815  mulgcd  12817  gcdzeq  12823  dvdsmulgcd  12826  sqgcd  12830  bezoutr  12833  lcmval  12865  lcmcllem  12869  gcddvdslcm  12875  lcmgcdlem  12879  lcmgcd  12880  lcmgcdeq  12885  lcmdvdsb  12886  mulgcddvds  12896  rpmulgcd2  12897  qredeu  12899  rpdvds  12901  isprm3  12920  divgcdodd  12946  coprm  12947  rpexp  12956  sqrt2irr  12965  qnumcl  12992  qnumdencoprm  12997  divnumden  13000  numsq  13007  phimullem  13031  eulerthlem1  13033  prmdiveq  13042  prmdivdiv  13043  hashgcdlem  13044  odzcl  13050  reumodprminv  13060  pythagtriplem19  13089  pclemub  13094  pcprendvds  13097  pcprendvds2  13098  pcpre1  13099  pcpremul  13100  pceulem  13101  pceu  13102  pczpre  13104  pczcl  13105  pcgcd1  13135  pc2dvds  13137  pcaddlem  13146  pcmpt  13150  pockthlem  13163  prmunb  13169  4sqlem7  13191  4sqlem8  13192  4sqlem9  13193  4sqlem10  13194  4sqlem14  13211  4sqlem15  13212  4sqlem16  13213  4sqlem17  13214  4sqlem18  13215  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemimin  13306  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsv  13310  ballotfilemsgt1  13311  ballotfilemsdom  13312  ballotfilemsel1i  13313  ballotfilemsf1o  13314  ballotfilemsi  13315  ballotfilemsima  13316  ballotfilemscr  13319  ballotfilemrv  13320  ballotfilemrv2  13322  ballotfilemro  13323  ballotfilemfrc  13327  ballotfilemfrci  13328  ballotfilemfrceq  13329  ballotfilemfrcn0  13330  ballotfilemrc  13331  ballotfilemirc  13332  ballotfilemrinv0  13333  ballotfilem1ri  13335  ennnfonelemg  13351  ennnfonelemf1  13366  ctiunctlemu1st  13382  nninfdclemf  13397  nninfdclemp1  13398  mgmidcl  13756  gzsumfzval  13769  gzsumval2  13772  mndlid  13806  imasmndf1  13819  dfgrp3mlem  13961  grplactf1o  13966  imasgrpf1  13973  subgsubm  14057  qusgrp  14093  ghmgrp1  14106  ghmf  14108  ghmnsgpreima  14130  kerf1ghm  14135  conjsubg  14138  resscntz  14165  gzsumsplit0  14237  gsumvalfi  14241  prdsmndd  14300  prdsgrpd  14303  prdsinvgd  14304  imasrng  14361  srgdilem  14379  srgdi  14384  srglidm  14389  ringdilem  14422  ringdi  14429  ringlidm  14434  imasring  14477  imasringf1  14478  dvdsrcld  14512  unitcld  14523  unitmulcl  14528  unitnegcl  14545  rhmghm  14577  elrhmunit  14592  subrgss  14638  subrgrcl  14642  rrgsupp  14682  lmodvscl  14749  lmodvsdi  14756  lmodvsdir  14757  lsslsp  14874  qusring  14972  crngridl  14975  znunit  15102  znrrg  15103  assaass  15112  assalmod  15114  psrbaglesuppg  15170  psrbagcon  15174  psrbagconcl  15176  gsumbagdiaglem  15184  gsumbagdiagfi  15185  psrass1filem  15186  psrelbas  15188  psraddcl  15193  rhmpsrfilem2  15194  psrmulfval  15196  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  mvrclfi  15226  mplrcl  15227  mplsubgfileminv  15233  uniopn  15244  restbasg  15411  cntop1  15444  cnf  15447  cnpf2  15450  lmtopcnp  15493  psmetdmdm  15567  psmetf  15568  psmet0  15570  xmetf  15593  metf  15594  blhalf  15651  xmetxpbl  15751  ioo2bl  15794  tgioo  15797  cncff  15820  rescncf  15824  cdivcncfap  15847  cnopnap  15854  divcncfap  15857  dedekindeulemeu  15865  dedekindicclemeu  15874  ivthinclemlm  15877  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthinclemdisj  15883  ivthdec  15887  ivthreinc  15888  limcimolemlt  15907  limcimo  15908  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  limccoap  15921  eldvap  15925  dvbsssg  15929  dvfgg  15931  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcj  15952  dvfre  15953  dvrecap  15956  plyco  16002  plycj  16004  sin0pilem1  16025  sin0pilem2  16026  pilem3  16027  tanrpcl  16081  tangtx  16082  zprmlogbaplem2  16233  zprmlogbaplem3  16234  ppiqsval2  16258  chtqge0  16264  chtqwordi  16280  chtublem  16312  perfect  16318  bposlem1  16328  bposlem4  16331  bposlem5  16332  bposlem9  16336  lgsne0  16379  lgseisen  16415  lgsquad2lem2  16423  2sqlem8a  16463  2sqlem8  16464  structgrssvtx  16505  edguhgr  16600  umgrpredgv  16610  umgrnloop2  16614  umgr2edg  16670  subuhgr  16735  subumgr  16737  subusgr  16738  wlkpropg  16787  wlkv  16789  wlkvtxeledgg  16807  wlkvtxiedgg  16809  wlk1walkdom  16822  trlsv  16847  clwwlksswrd  16860  clwwlkclwwlkn  16872  eupthv  16909  eupthseg  16915  eupth2lem3lem3fi  16933  eupth2lem3lem4fi  16936  eupth2lemsfi  16941  eulerpathprum  16943  nninfalllem1  17274  iooref1o  17306  als1d  17357  rals1d  17359  alseu1d  17393  ralseu1d  17395