Theorem 3adant1r 1226

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant1r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3expb 1199	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	adantlr 474	. 2 |- ( ( ( ph /\ ta ) /\ ( ps /\ ch ) ) -> th )
4	3	3impb 1194	1 |- ( ( ( ph /\ ta ) /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3adant2r  1228  3adant3r  1230  tfr1onlembacc  6321  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  tfrcl  6343  mulassnqg  7346  prarloc  7465  prmuloc  7528  addasssrg  7718  axaddass  7834