Theorem 3ad2ant2 803

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

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  mopick2 1439  fnco 3601  oprssoprval 4040  omass 4217  cnegextlem2 5358  xrre2t 5582  divne0bt 5735  lt2mul2divt 5874  lediv2t 5893  nndivtrt 5962  supxrun 6087  gtndivt 6195  qbtwnre 6279  ubicc2t 6406  icoshftf1olem 6411  eluzp1p1t 6436  peano2uz 6448  seqzm1 6550  seqzval2t 6554  expnbndt 6655  absrpclt 6855  seq1ub 6912  bccmplt 6962  climrecl 7110  cvgratlem5 7254  tgtop11t 7633  tgsst 7635  iincld 7676  elnei 7722  cnconst 7777  metcnpf 7880  metcnp 7884  metdnsconst 7898  caussi 7951  bcthlem9 8004  resgrprn 8091  nvsge0 8287  nvcnpf 8324  nvcnpi3 8418  nvcnpi4 8419  nmoub2i 8433  isblo3i 8457  ipassr2 8503  efifolem5 8721  bcs2t 9044  elspansn2t 9485  fh2t 9557  pjoi0t 9657  adjeqt 9854  leopmult 10062  mdslmd4 10255  cdj3lem2 10357  ghomfo 10386  ghomid 10389  truni1 10485  homcard 10525  hmeobc 10528  filintf 10554  fgsb 10555  fgsb2 10560  rcfpfillem6 10568  mslb1 10600  2wsms 10601  idosd 10648  1cat 10663  imonclem 10712  cmpmon 10714  icmpmon 10715  idmon 10716

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 779

Copyright terms: Public domain