Theorem 3ad2ant2 799

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

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  mopick2 1429  fnco 3581  oprssoprval 4019  omass 4195  cnegextlem2 5318  xrre2t 5543  divne0bt 5691  lt2mul2divt 5822  lediv2t 5839  nndivtrt 5907  supxrun 6032  gtndivt 6140  qbtwnre 6216  ubicc2t 6338  icoshftf1olem 6343  eluzp1p1t 6367  peano2uz 6379  seqzm1 6481  seqzval2t 6485  expnbndt 6585  absrpclt 6790  seq1ub 6849  bccmplt 6900  climrecl 7047  cvgratlem5 7189  tgtop11t 7576  tgsst 7578  iincld 7621  elnei 7666  cnconst 7719  metcnpf 7822  metcnp 7826  metdnsconst 7840  caussi 7889  bcthlem9 7941  resgrprn 8030  nvsge0 8230  nvcnpi4 8355  nmoub2i 8369  isblo3i 8392  ipassr2 8438  efifolem5 8641  bcs2t 8970  elspansn2t 9406  fh2t 9479  pjoi0t 9579  adjeqt 9775  leopmult 9979  mdslmd4 10168  cdj3lem2 10267  ghomfo 10296  ghomid 10299  truni1 10386  homcard 10426  filintf 10443  fgsb 10444  fgsb2 10449  mslb1 10473  2wsms 10474  idosd 10521  1cat 10536  imonclem 10583  cmpmon 10585  icmpmon 10587  idmon 10588

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 775

Copyright terms: Public domain