Theorem 3adant3r1 1243

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)

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 1235	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr1 1187	1 |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ccatswrd  11458  imasmnd2  13812  grpsubsub  13947  grpnnncan2  13955  imasgrp2  13966  mulgnn0ass  14014  mulgsubdir  14018  cmn32  14191  ablsubadd  14200  imasrng  14339  imasring  14453  opprrng  14466  opprring  14468  xmettri3  15566  mettri3  15567  xmetrtri  15568  rprelogbmulexp  16153