Theorem 3ad2ant3 802

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 797	1 |- ((ps /\ th /\ ph) -> ch)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  limsuc 3120  oprabvalig 4024  curry1val 4100  omwordi 4202  oneo 4212  oewordi 4218  cnegextlem2 5346  divcan5t 5781  lemul1it 5837  lemul1itOLD 5838  lt2mul2divt 5872  lediv2t 5891  lt2halvest 6042  infmrcl 6069  elioo5t 6384  iccsupr 6398  iccnegt 6407  icoshft 6408  icoshftf1olem 6410  elfzlem 6473  fzshftralt 6522  serzmulc1 7057  climge0 7112  rescncf 7272  mulc1cncf 7279  demoivre 7484  tgsst 7636  clsss 7687  ntrcls0 7707  neiss 7723  neips 7727  cnpval 7759  elbl2 7839  lmbrf 7930  iscms2lem3 7991  grplactval 8097  vcid 8170  vcdi 8171  vcdir 8172  vcass 8173  imsmetlem 8323  nmoval 8426  nmoubi 8435  0oval 8448  spwval3 8654  spwnex3 8655  sincosq1eq 8709  nmopubt 9832  nmfnleubt 9849  hmopcot 9948  nmcopexlem5 9955  nmcfnexlem5 9984  adjlnopt 10019  mdslmd4 10260  ghomf1olem 10396  nnssi3 10420  ompfl3 10427  oprabvaligg 10440  elo 10444  infi1 10447  infi1OLD 10448  ishomeo 10517  hmphsyma 10528  filintf 10569  fgsb 10570  fgsbOLD 10571  cnfilca 10583  cnfilcaOLD 10584  rcfpfil 10597  rcfpfilOLD 10598  cmppfd 10678  1cat 10692  imonclem 10741  ismonc 10742  isfunb 10755

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 777

Copyright terms: Public domain