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  11463  imasmnd2  13817  grpsubsub  13952  grpnnncan2  13960  imasgrp2  13971  mulgnn0ass  14019  mulgsubdir  14023  cmn32  14196  ablsubadd  14205  imasrng  14361  imasring  14477  opprrng  14490  opprring  14492  xmettri3  15617  mettri3  15618  xmetrtri  15619  rprelogbmulexp  16209