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  3224  unssad  3398  opth1  4354  opth  4355  0nelop  4366  epelg  4413  poirr  4430  brrelex1  4791  brrelex  4792  asymref  5150  soirri  5159  sotri  5160  ffdmd  5536  fcnvres  5552  fun11iun  5637  funopsn  5862  elmpocl1  6252  f1od  6260  f1o2d  6262  oprssdmm  6367  elmpom  6436  fczsupp0  6461  smoiso  6535  tfrlem1  6541  swoer  6797  ecopovtrn  6868  ecopovtrng  6871  elmapssres  6909  pmresg  6912  mapsspm  6918  en1uniel  7046  pw2f1odc  7090  xpf1o  7099  sbthlemi9  7237  fsuppfund  7249  supelti  7295  supsnti  7298  supisoti  7303  ctssdccl  7404  ctfoex  7411  fodjum  7439  en2eleq  7500  djuen  7520  pw1if  7537  dftap2  7567  2omotaplemst  7574  exmidapne  7576  ccfunen  7580  dfplpq2  7671  ltbtwnnqq  7732  enq0tr  7751  elnp1st2nd  7793  prcdnql  7801  prnminu  7806  prloc  7808  genpcdl  7836  addnqprulem  7845  addlocprlemlt  7848  addlocprlemgt  7851  addlocprlem  7852  addlocpr  7853  nqprxx  7863  ltnqex  7866  addnqprlemfl  7876  addnqprlemfu  7877  appdivnq  7880  prmuloclemcalc  7882  prmuloc  7883  mullocprlem  7887  mulnqprlemfl  7892  mulnqprlemfu  7893  ltprordil  7906  ltnqpri  7911  ltexprlemm  7917  ltexprlemopl  7918  ltexprlemlol  7919  ltexprlemopu  7920  ltexprlemupu  7921  ltexprlemdisj  7923  ltexprlemloc  7924  ltexprlemfl  7926  ltexprlemrl  7927  ltexprlemfu  7928  ltexprlemru  7929  ltexpri  7930  lteupri  7934  ltaprlem  7935  recexprlemell  7939  recexprlemelu  7940  recexprlemloc  7948  recexprlempr  7949  recexprlem1ssl  7950  recexprlem1ssu  7951  recexprlemss1u  7953  aptipr  7958  cauappcvgprlemm  7962  cauappcvgprlemlol  7964  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  cauappcvgprlemladdru  7973  cauappcvgprlem1  7976  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprlemm  7985  caucvgprlemlol  7987  caucvgprlemladdfu  7994  caucvgprprlemloccalc  8001  caucvgprprlemnkltj  8006  caucvgprprlemnbj  8010  caucvgprprlemml  8011  caucvgprprlemlol  8015  caucvgprprlemloc  8020  caucvgprprlemexbt  8023  suplocexprlemss  8032  suplocexprlemru  8036  suplocexprlemlub  8041  ltsrprg  8064  caucvgsrlemasr  8107  suplocsrlemb  8123  suplocsrlem  8125  suplocsr  8126  axcaucvglemcau  8215  axpre-suploclemres  8218  negf1o  8657  apreap  8863  apreim  8879  msqge0  8892  mulge0  8895  apti  8898  apsscn  8923  mulap0bad  8935  divadddivap  9003  recnz  9674  lbzbi  9951  xadd4d  10221  ixxss1  10240  ixxss2  10241  ixxss12  10242  iccss2  10280  iccssioo2  10282  iccssico2  10283  iccen  10343  elfzole1  10494  ioom  10624  elicore  10630  flqle  10642  flqltnz  10651  addmodlteq  10764  expclzap  10930  hashennnuni  11146  zfz1isolem1  11216  hashdmprop2dom  11220  swrdsbslen  11362  ccatswrd  11366  ccatpfx  11397  recl  11542  cvg1nlemcau  11673  cvg1nlemres  11674  resqrtth  11720  fimaxre2  11916  climcl  11971  reccn2ap  12002  nnf1o  12066  summodclem3  12070  sumpr  12103  fsump1i  12123  fisumcom2  12128  fsum00  12152  fsumparts  12160  mertenslemi1  12225  prodmodclem3  12265  fprodcom2fi  12316  addsin  12432  subsin  12433  addcos  12436  subcos  12437  sinbnd2  12444  cosbnd2  12445  sin01gt0  12452  cos01gt0  12453  divgcdz  12671  divgcdnn  12675  gcdaddm  12684  bezoutlemstep  12697  dvdsgcdb  12713  dfgcd2  12714  mulgcd  12716  gcdzeq  12722  dvdsmulgcd  12725  sqgcd  12729  bezoutr  12732  lcmval  12764  lcmcllem  12768  gcddvdslcm  12774  lcmgcdlem  12778  lcmgcd  12779  lcmgcdeq  12784  lcmdvdsb  12785  mulgcddvds  12795  rpmulgcd2  12796  qredeu  12798  rpdvds  12800  isprm3  12819  divgcdodd  12844  coprm  12845  rpexp  12854  sqrt2irr  12863  qnumcl  12889  qnumdencoprm  12894  divnumden  12897  numsq  12904  phimullem  12926  eulerthlem1  12928  prmdiveq  12937  prmdivdiv  12938  hashgcdlem  12939  odzcl  12945  reumodprminv  12955  pythagtriplem19  12984  pclemub  12989  pcprendvds  12992  pcprendvds2  12993  pcpre1  12994  pcpremul  12995  pceulem  12996  pceu  12997  pczpre  12999  pczcl  13000  pcgcd1  13030  pc2dvds  13032  pcaddlem  13041  pcmpt  13045  pockthlem  13058  prmunb  13064  4sqlem7  13086  4sqlem8  13087  4sqlem9  13088  4sqlem10  13089  4sqlem14  13106  4sqlem15  13107  4sqlem16  13108  4sqlem17  13109  4sqlem18  13110  ballotfilem2  13149  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilem4  13159  ennnfonelemg  13171  ennnfonelemf1  13186  ctiunctlemu1st  13202  nninfdclemf  13217  nninfdclemp1  13218  mgmidcl  13608  gsumfzval  13621  gsumval2  13627  mndlid  13665  prdsmndd  13678  imasmndf1  13684  dfgrp3mlem  13828  grplactf1o  13833  prdsgrpd  13839  prdsinvgd  13840  imasgrpf1  13846  subgsubm  13930  qusgrp  13966  ghmgrp1  13979  ghmf  13981  ghmnsgpreima  14003  kerf1ghm  14008  conjsubg  14011  gsumsplit0  14080  imasrng  14117  srgdilem  14130  srgdi  14135  srglidm  14140  ringdilem  14173  ringdi  14179  ringlidm  14184  imasring  14225  imasringf1  14226  dvdsrcld  14259  unitcld  14270  unitmulcl  14275  unitnegcl  14292  rhmghm  14324  elrhmunit  14339  subrgss  14384  subrgrcl  14388  rrgsupp  14428  lmodvscl  14470  lmodvsdi  14476  lmodvsdir  14477  lsslsp  14594  qusring  14692  crngridl  14695  znunit  14824  znrrg  14825  psrbaglesuppg  14838  psrbagcon  14843  psrbagconcl  14844  psrelbas  14847  psraddcl  14852  mplrcl  14866  uniopn  14883  restbasg  15050  cntop1  15083  cnf  15086  cnpf2  15089  lmtopcnp  15132  psmetdmdm  15206  psmetf  15207  psmet0  15209  xmetf  15232  metf  15233  blhalf  15290  xmetxpbl  15390  ioo2bl  15433  tgioo  15436  cncff  15459  rescncf  15463  cdivcncfap  15486  cnopnap  15493  divcncfap  15496  dedekindeulemeu  15504  dedekindicclemeu  15513  ivthinclemlm  15516  ivthinclemlopn  15518  ivthinclemuopn  15520  ivthinclemdisj  15522  ivthdec  15526  ivthreinc  15527  limcimolemlt  15546  limcimo  15547  limccnpcntop  15557  limccnp2lem  15558  limccnp2cntop  15559  limccoap  15560  eldvap  15564  dvbsssg  15568  dvfgg  15570  dvaddxxbr  15583  dvmulxxbr  15584  dvcoapbr  15589  dvcj  15591  dvfre  15592  dvrecap  15595  plyco  15641  plycj  15643  sin0pilem1  15663  sin0pilem2  15664  pilem3  15665  tanrpcl  15719  tangtx  15720  perfect  15886  lgsne0  15928  lgseisen  15964  lgsquad2lem2  15972  2sqlem8a  16012  2sqlem8  16013  structgrssvtx  16054  edguhgr  16149  umgrpredgv  16159  umgrnloop2  16163  umgr2edg  16219  subuhgr  16284  subumgr  16286  subusgr  16287  wlkpropg  16336  wlkv  16338  wlkvtxeledgg  16356  wlkvtxiedgg  16358  wlk1walkdom  16371  trlsv  16396  clwwlksswrd  16409  clwwlkclwwlkn  16421  eupthv  16458  eupthseg  16464  eupth2lem3lem3fi  16482  eupth2lem3lem4fi  16485  eupth2lemsfi  16490  eulerpathprum  16492  nninfalllem1  16803  iooref1o  16835  gfsumval  16879  alsi1d  16895  alsc1d  16897