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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem is referenced by:  bi1  117  simplbi  270  simprbda  378  simp1  964  eldifad  3048  unssad  3219  opth1  4118  opth  4119  0nelop  4130  epelg  4172  poirr  4189  brrelex1  4538  brrelex  4539  asymref  4882  soirri  4891  sotri  4892  fcnvres  5264  fun11iun  5344  elmpocl1  5923  f1od  5927  f1o2d  5929  oprssdmm  6023  smoiso  6153  tfrlem1  6159  swoer  6411  ecopovtrn  6480  ecopovtrng  6483  elmapssres  6521  pmresg  6524  mapsspm  6530  en1uniel  6652  xpf1o  6691  sbthlemi9  6805  supelti  6841  supsnti  6844  supisoti  6849  ctssdccl  6948  fodjum  6968  en2eleq  6999  djuen  7015  ccfunen  7027  dfplpq2  7110  ltbtwnnqq  7171  enq0tr  7190  elnp1st2nd  7232  prcdnql  7240  prnminu  7245  prloc  7247  genpcdl  7275  addnqprulem  7284  addlocprlemlt  7287  addlocprlemgt  7290  addlocprlem  7291  addlocpr  7292  nqprxx  7302  ltnqex  7305  addnqprlemfl  7315  addnqprlemfu  7316  appdivnq  7319  prmuloclemcalc  7321  prmuloc  7322  mullocprlem  7326  mulnqprlemfl  7331  mulnqprlemfu  7332  ltprordil  7345  ltnqpri  7350  ltexprlemm  7356  ltexprlemopl  7357  ltexprlemlol  7358  ltexprlemopu  7359  ltexprlemupu  7360  ltexprlemdisj  7362  ltexprlemloc  7363  ltexprlemfl  7365  ltexprlemrl  7366  ltexprlemfu  7367  ltexprlemru  7368  ltexpri  7369  lteupri  7373  ltaprlem  7374  recexprlemell  7378  recexprlemelu  7379  recexprlemloc  7387  recexprlempr  7388  recexprlem1ssl  7389  recexprlem1ssu  7390  recexprlemss1u  7392  aptipr  7397  cauappcvgprlemm  7401  cauappcvgprlemlol  7403  cauappcvgprlemladdfu  7410  cauappcvgprlemladdfl  7411  cauappcvgprlemladdru  7412  cauappcvgprlem1  7415  caucvgprlemnkj  7422  caucvgprlemnbj  7423  caucvgprlemm  7424  caucvgprlemlol  7426  caucvgprlemladdfu  7433  caucvgprprlemloccalc  7440  caucvgprprlemnkltj  7445  caucvgprprlemnbj  7449  caucvgprprlemml  7450  caucvgprprlemlol  7454  caucvgprprlemloc  7459  caucvgprprlemexbt  7462  ltsrprg  7490  caucvgsrlemasr  7532  axcaucvglemcau  7633  negf1o  8063  apreap  8267  apreim  8283  msqge0  8296  mulge0  8299  apti  8302  mulap0bad  8333  divadddivap  8400  recnz  9048  lbzbi  9310  xadd4d  9561  ixxss1  9580  ixxss2  9581  ixxss12  9582  iccss2  9620  iccssioo2  9622  iccssico2  9623  elfzole1  9825  ioom  9931  flqle  9944  flqltnz  9953  addmodlteq  10064  expclzap  10211  hashennnuni  10418  zfz1isolem1  10476  recl  10518  cvg1nlemcau  10648  cvg1nlemres  10649  resqrtth  10695  fimaxre2  10890  climcl  10943  reccn2ap  10974  isummolemnm  11040  summodclem3  11041  sumpr  11074  fsump1i  11094  fisumcom2  11099  fsum00  11123  fsumparts  11131  mertenslemi1  11196  addsin  11300  subsin  11301  addcos  11304  subcos  11305  sinbnd2  11312  cosbnd2  11313  sin01gt0  11319  cos01gt0  11320  divgcdz  11508  divgcdnn  11511  gcdaddm  11520  bezoutlemstep  11531  dvdsgcdb  11547  dfgcd2  11548  mulgcd  11550  gcdzeq  11556  dvdsmulgcd  11559  sqgcd  11563  bezoutr  11566  lcmval  11590  lcmcllem  11594  gcddvdslcm  11600  lcmgcdlem  11604  lcmgcd  11605  lcmgcdeq  11610  lcmdvdsb  11611  mulgcddvds  11621  rpmulgcd2  11622  qredeu  11624  rpdvds  11626  isprm3  11645  divgcdodd  11667  coprm  11668  rpexp  11677  sqrt2irr  11686  qnumcl  11711  qnumdencoprm  11716  divnumden  11719  numsq  11726  phimullem  11746  hashgcdlem  11748  ennnfonelemg  11761  ennnfonelemf1  11776  ctiunctlemu1st  11790  uniopn  12011  restbasg  12180  cntop1  12212  cnf  12215  cnpf2  12218  lmtopcnp  12261  psmetdmdm  12313  psmetf  12314  psmet0  12316  xmetf  12339  metf  12340  blhalf  12397  xmetxpbl  12497  ioo2bl  12529  tgioo  12532  cncff  12550  rescncf  12554  cdivcncfap  12573  limcimolemlt  12589  limcimo  12590  limccnpcntop  12600  limccnp2lem  12601  limccnp2cntop  12602  eldvap  12606  dvbsssg  12610  dvfgg  12612  dvaddxxbr  12620  dvmulxxbr  12621  nninfalllem1  12895  alsi1d  12938  alsc1d  12940