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  11464  imasmnd2  13818  grpsubsub  13953  grpnnncan2  13961  imasgrp2  13972  mulgnn0ass  14020  mulgsubdir  14024  cmn32  14197  ablsubadd  14206  imasrng  14362  imasring  14478  opprrng  14491  opprring  14493  xmettri3  15600  mettri3  15601  xmetrtri  15602  rprelogbmulexp  16192