Theorem 3adant3r1 842

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
3exp.1	|- ((ph /\ ps /\ ch) -> th)

Assertion

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

Proof of Theorem 3adant3r1

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3expb 834	. 2 |- ((ph /\ (ps /\ ch)) -> th)
3	2	3adantr1 806	1 |- ((ph /\ (ta /\ ps /\ ch)) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  mettri3 7818  grpdivdiv 8087  grpmuldivass 8088  grppnpcan2 8092  grpnnncan2 8093  abl23 8104  abldivdiv4 8109  abldiv23 8110  ablnnncan 8111  nvmdi 8270  nvsubsub23 8282  nvmtri2 8300  ipdi 8503  ipassr 8506  ipsubdir 8508  ipsubdi 8509  cmpassoh 10729  homgrf 10730

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