Theorem simpld 110

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  bi1  116  simplbi  268  simprbda  375  simp1  941  eldifad  2999  unssad  3166  opth1  4037  opth  4038  0nelop  4049  epelg  4091  poirr  4108  brrelex  4448  asymref  4784  soirri  4793  sotri  4794  fcnvres  5157  fun11iun  5237  elmpt2cl1  5800  f1od  5804  f1o2d  5806  smoiso  6021  tfrlem1  6027  swoer  6272  ecopovtrn  6341  ecopovtrng  6344  elmapssres  6382  pmresg  6385  mapsspm  6391  en1uniel  6473  xpf1o  6512  sbthlemi9  6618  supelti  6641  supsnti  6644  supisoti  6649  fodjuomnilemm  6745  en2eleq  6765  dfplpq2  6857  ltbtwnnqq  6918  enq0tr  6937  elnp1st2nd  6979  prcdnql  6987  prnminu  6992  prloc  6994  genpcdl  7022  addnqprulem  7031  addlocprlemlt  7034  addlocprlemgt  7037  addlocprlem  7038  addlocpr  7039  nqprxx  7049  ltnqex  7052  addnqprlemfl  7062  addnqprlemfu  7063  appdivnq  7066  prmuloclemcalc  7068  prmuloc  7069  mullocprlem  7073  mulnqprlemfl  7078  mulnqprlemfu  7079  ltprordil  7092  ltnqpri  7097  ltexprlemm  7103  ltexprlemopl  7104  ltexprlemlol  7105  ltexprlemopu  7106  ltexprlemupu  7107  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  ltexpri  7116  lteupri  7120  ltaprlem  7121  recexprlemell  7125  recexprlemelu  7126  recexprlemloc  7134  recexprlempr  7135  recexprlem1ssl  7136  recexprlem1ssu  7137  recexprlemss1u  7139  aptipr  7144  cauappcvgprlemm  7148  cauappcvgprlemlol  7150  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlem1  7162  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemlol  7173  caucvgprlemladdfu  7180  caucvgprprlemloccalc  7187  caucvgprprlemnkltj  7192  caucvgprprlemnbj  7196  caucvgprprlemml  7197  caucvgprprlemlol  7201  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  ltsrprg  7237  caucvgsrlemasr  7279  axcaucvglemcau  7377  negf1o  7804  apreap  8005  apreim  8021  msqge0  8034  mulge0  8037  apti  8040  mulap0bad  8067  divadddivap  8133  recnz  8772  lbzbi  9033  ixxss1  9254  ixxss2  9255  ixxss12  9256  iccss2  9294  iccssioo2  9296  iccssico2  9297  elfzole1  9494  ioom  9600  flqle  9613  flqltnz  9622  addmodlteq  9733  expclzap  9878  hashennnuni  10083  zfz1isolem1  10141  recl  10182  cvg1nlemcau  10312  cvg1nlemres  10313  resqrtth  10359  fimaxre2  10551  climcl  10563  isummolemnm  10658  isummolem3  10659  divgcdz  10838  divgcdnn  10841  gcdaddm  10850  bezoutlemstep  10861  dvdsgcdb  10877  dfgcd2  10878  mulgcd  10880  gcdzeq  10886  dvdsmulgcd  10889  sqgcd  10893  bezoutr  10896  lcmval  10920  lcmcllem  10924  gcddvdslcm  10930  lcmgcdlem  10934  lcmgcd  10935  lcmgcdeq  10940  lcmdvdsb  10941  mulgcddvds  10951  rpmulgcd2  10952  qredeu  10954  rpdvds  10956  isprm3  10975  divgcdodd  10997  coprm  10998  rpexp  11007  sqrt2irr  11016  qnumcl  11041  qnumdencoprm  11046  divnumden  11049  numsq  11056  phimullem  11076  hashgcdlem  11078  nninfalllem1  11337  alsi1d  11360  alsc1d  11362