Theorem 3ad2ant2 801

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantr 389	. 2 |- ((ph /\ th) -> ch)
3	2	3adant1 797	1 |- ((ps /\ ph /\ th) -> ch)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  mopick2 1436  fnco 3595  oprssoprval 4034  omass 4211  cnegextlem2 5346  xrre2t 5570  divne0bt 5728  lt2mul2divt 5872  lediv2t 5891  nndivtrt 5960  supxrun 6085  gtndivt 6193  qbtwnre 6278  ubicc2t 6405  icoshftf1olem 6410  eluzp1p1t 6435  peano2uz 6447  seqzm1 6549  seqzval2t 6553  expnbndt 6654  mulretOLD 6777  absrpclt 6855  seq1ub 6912  bccmplt 6962  climrecl 7110  cvgratlem5 7254  tgtop11t 7634  tgsst 7636  iincld 7679  elnei 7725  cnconst 7780  metcnpf 7883  metcnp 7887  metdnsconst 7901  caussi 7954  bcthlem9 8007  resgrprn 8095  nvsge0 8291  nvcnpf 8328  nvcnpi3 8422  nvcnpi4 8423  nmoub2i 8437  isblo3i 8461  ipassr2 8507  efifolem5 8726  bcs2t 9049  elspansn2t 9490  fh2t 9562  pjoi0t 9662  adjeqt 9859  leopmult 10067  mdslmd4 10260  cdj3lem2 10362  ghomfo 10391  ghomid 10394  truni1 10499  homcard 10539  hmeobc 10542  filintf 10569  fgsb 10570  fgsbOLD 10571  fgsb2 10580  rcfpfillem6 10595  rcfpfillem6OLD 10596  mslb1 10629  2wsms 10630  idosd 10677  1cat 10692  imonclem 10741  cmpmon 10743  icmpmon 10744  idmon 10745

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