Theorem 3ad2ant3 801

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 388	. 2 |- ((th /\ ph) -> ch)
3	2	3adant1 796	1 |- ((ps /\ th /\ ph) -> ch)

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  limsuc 3115  oprabvalig 4015  curry1val 4090  omwordi 4192  oneo 4202  oewordi 4208  cnegextlem2 5326  divcan5t 5745  lemul1it 5801  lemul1itOLD 5802  lt2mul2divt 5830  lediv2t 5847  lt2halvest 5997  infmrcl 6024  iccsupr 6339  ioonegt 6347  iccnegt 6348  icoshft 6349  icoshftf1olem 6351  elfzlem 6413  fzshftralt 6462  serzmulc1 7003  climge0 7057  rescncf 7215  mulc1cncf 7222  demoivre 7434  tgsst 7586  clsss 7637  ntrcls0 7657  neiss 7673  neips 7677  cnpval 7709  elbl2 7791  lmbrf 7882  iscms2lem3 7941  grplactval 8048  vcid 8122  vcdi 8123  vcdir 8124  vcass 8125  imsmetlem 8274  nmoval 8371  nmoubi 8380  0oval 8393  spwval3 8596  spwnex3 8597  sincosq1eq 8645  nmopubt 9772  nmfnleubt 9788  hmopcot 9886  nmcopexlem5 9893  nmcfnexlem5 9922  adjlnopt 9957  mdslmd4 10197  ghomf1olem 10330  nnssi3 10356  oprabvaligg 10377  elo 10381  infi1 10383  ishomeo 10440  hmphsyma 10451  filintf 10479  fgsb 10480  cnfilca 10487  cmppfd 10558  1cat 10572  imonclem 10619  ismonc 10620  isfunb 10629

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 147  df-an 225  df-3an 776

Copyright terms: Public domain