Theorem simpld 111

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem is referenced by:  bi1  117  simplbi  272  simprbda  380  simp1  981  eldifad  3077  unssad  3248  opth1  4153  opth  4154  0nelop  4165  epelg  4207  poirr  4224  brrelex1  4573  brrelex  4574  asymref  4919  soirri  4928  sotri  4929  fcnvres  5301  fun11iun  5381  elmpocl1  5962  f1od  5966  f1o2d  5968  oprssdmm  6062  smoiso  6192  tfrlem1  6198  swoer  6450  ecopovtrn  6519  ecopovtrng  6522  elmapssres  6560  pmresg  6563  mapsspm  6569  en1uniel  6691  xpf1o  6731  sbthlemi9  6846  supelti  6882  supsnti  6885  supisoti  6890  ctssdccl  6989  ctfoex  6996  fodjum  7011  en2eleq  7044  djuen  7060  ccfunen  7072  dfplpq2  7155  ltbtwnnqq  7216  enq0tr  7235  elnp1st2nd  7277  prcdnql  7285  prnminu  7290  prloc  7292  genpcdl  7320  addnqprulem  7329  addlocprlemlt  7332  addlocprlemgt  7335  addlocprlem  7336  addlocpr  7337  nqprxx  7347  ltnqex  7350  addnqprlemfl  7360  addnqprlemfu  7361  appdivnq  7364  prmuloclemcalc  7366  prmuloc  7367  mullocprlem  7371  mulnqprlemfl  7376  mulnqprlemfu  7377  ltprordil  7390  ltnqpri  7395  ltexprlemm  7401  ltexprlemopl  7402  ltexprlemlol  7403  ltexprlemopu  7404  ltexprlemupu  7405  ltexprlemdisj  7407  ltexprlemloc  7408  ltexprlemfl  7410  ltexprlemrl  7411  ltexprlemfu  7412  ltexprlemru  7413  ltexpri  7414  lteupri  7418  ltaprlem  7419  recexprlemell  7423  recexprlemelu  7424  recexprlemloc  7432  recexprlempr  7433  recexprlem1ssl  7434  recexprlem1ssu  7435  recexprlemss1u  7437  aptipr  7442  cauappcvgprlemm  7446  cauappcvgprlemlol  7448  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  cauappcvgprlem1  7460  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemm  7469  caucvgprlemlol  7471  caucvgprlemladdfu  7478  caucvgprprlemloccalc  7485  caucvgprprlemnkltj  7490  caucvgprprlemnbj  7494  caucvgprprlemml  7495  caucvgprprlemlol  7499  caucvgprprlemloc  7504  caucvgprprlemexbt  7507  suplocexprlemss  7516  suplocexprlemru  7520  suplocexprlemlub  7525  ltsrprg  7548  caucvgsrlemasr  7591  suplocsrlemb  7607  suplocsrlem  7609  suplocsr  7610  axcaucvglemcau  7699  axpre-suploclemres  7702  negf1o  8137  apreap  8342  apreim  8358  msqge0  8371  mulge0  8374  apti  8377  apsscn  8402  mulap0bad  8413  divadddivap  8480  recnz  9137  lbzbi  9401  xadd4d  9661  ixxss1  9680  ixxss2  9681  ixxss12  9682  iccss2  9720  iccssioo2  9722  iccssico2  9723  elfzole1  9925  ioom  10031  flqle  10044  flqltnz  10053  addmodlteq  10164  expclzap  10311  hashennnuni  10518  zfz1isolem1  10576  recl  10618  cvg1nlemcau  10749  cvg1nlemres  10750  resqrtth  10796  fimaxre2  10991  climcl  11044  reccn2ap  11075  isummolemnm  11141  summodclem3  11142  sumpr  11175  fsump1i  11195  fisumcom2  11200  fsum00  11224  fsumparts  11232  mertenslemi1  11297  addsin  11438  subsin  11439  addcos  11442  subcos  11443  sinbnd2  11450  cosbnd2  11451  sin01gt0  11457  cos01gt0  11458  divgcdz  11649  divgcdnn  11652  gcdaddm  11661  bezoutlemstep  11674  dvdsgcdb  11690  dfgcd2  11691  mulgcd  11693  gcdzeq  11699  dvdsmulgcd  11702  sqgcd  11706  bezoutr  11709  lcmval  11733  lcmcllem  11737  gcddvdslcm  11743  lcmgcdlem  11747  lcmgcd  11748  lcmgcdeq  11753  lcmdvdsb  11754  mulgcddvds  11764  rpmulgcd2  11765  qredeu  11767  rpdvds  11769  isprm3  11788  divgcdodd  11810  coprm  11811  rpexp  11820  sqrt2irr  11829  qnumcl  11855  qnumdencoprm  11860  divnumden  11863  numsq  11870  phimullem  11890  hashgcdlem  11892  ennnfonelemg  11905  ennnfonelemf1  11920  ctiunctlemu1st  11936  uniopn  12157  restbasg  12326  cntop1  12359  cnf  12362  cnpf2  12365  lmtopcnp  12408  psmetdmdm  12482  psmetf  12483  psmet0  12485  xmetf  12508  metf  12509  blhalf  12566  xmetxpbl  12666  ioo2bl  12701  tgioo  12704  cncff  12722  rescncf  12726  cdivcncfap  12745  cnopnap  12752  dedekindeulemeu  12758  dedekindicclemeu  12767  ivthinclemlm  12770  ivthinclemlopn  12772  ivthinclemuopn  12774  ivthinclemdisj  12776  ivthdec  12780  limcimolemlt  12791  limcimo  12792  limccnpcntop  12802  limccnp2lem  12803  limccnp2cntop  12804  limccoap  12805  eldvap  12809  dvbsssg  12813  dvfgg  12815  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcj  12831  dvfre  12832  dvrecap  12835  sin0pilem1  12851  sin0pilem2  12852  pilem3  12853  tanrpcl  12907  tangtx  12908  nninfalllem1  13192  alsi1d  13236  alsc1d  13238