Theorem 3adant1r 1221

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 1194	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	adantlr 469	. 2 |- ( ( ( ph /\ ta ) /\ ( ps /\ ch ) ) -> th )
4	3	3impb 1189	1 |- ( ( ( ph /\ ta ) /\ ps /\ ch ) -> th )

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

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 970

This theorem is referenced by:  3adant2r  1223  3adant3r  1225  tfr1onlembacc  6310  tfr1onlembfn  6312  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllembfn  6325  tfrcllemaccex  6329  tfrcllemres  6330  tfrcldm  6331  tfrcl  6332  mulassnqg  7325  prarloc  7444  prmuloc  7507  addasssrg  7697  axaddass  7813