Theorem 3ad2ant3 814

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
3ad2ant.1	|- (ph -> ch)

Assertion

Ref	Expression
3ad2ant3	|- ((ps /\ th /\ ph) -> ch)

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantl 397	. 2 |- ((th /\ ph) -> ch)
3	2	3adant1 809	1 |- ((ps /\ th /\ ph) -> ch)

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  limsuc 3177  oprabvalig 4082  curry1val 4158  omwordi 4260  oneo 4270  oewordi 4276  cnegexlem2 5411  divcan5 5839  lemul1a 5895  lemul1aOLD 5896  lt2mul2div 5931  lediv2 5951  lt2halves 6103  infmrcl 6151  zdivmul 6272  modcyc 6376  modcycOLD 6377  elioo5 6409  iccsupr 6424  iccneg 6433  icoshf 6434  icoshftf1olem 6436  elfzlem 6499  fzshftral 6548  serzmulc1 7147  climge0 7202  rescncf 7362  mulc1cncf 7369  demoivre 7576  tgss 7725  clsss 7772  ntrcls0 7792  neiss 7808  neips 7812  cnpval 7844  elbl2 7924  lmbrf 8015  iscms2lem3 8076  grplactval 8181  vcid 8254  vcdi 8255  vcdir 8256  vcass 8257  imsmetlem 8407  nmoval 8510  nmoubi 8519  0oval 8532  spwval3 8738  spwnex3 8739  sincosq1eq 8792  nmopub 9915  nmfnleub 9932  hmopco 10031  nmcopexlem5 10038  nmcfnexlem5 10067  adjlnop 10102  mdslmd4i 10344  ghomf1olem 10481  nnssi3 10507  ompfl3 10514  oprabvaligg 10526  elo 10530  infi1 10532  inposet 10578  ishomeo 10611  hmphsyma 10622  filintf 10662  fgsb 10663  cnfilca 10670  rcfpfil 10677  usinuniop 10703  cmppfd 10760  1cat 10774  imonclem 10823  ismonc 10824  iepiclem 10833  isepic 10834  isfunb 10839

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232  df-3an 789

Copyright terms: Public domain