Theorem 3adant1r 1209

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

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

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 964

This theorem is referenced by:  3adant2r  1211  3adant3r  1213  tfr1onlembacc  6232  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllembfn  6247  tfrcllemaccex  6251  tfrcllemres  6252  tfrcldm  6253  tfrcl  6254  mulassnqg  7185  prarloc  7304  prmuloc  7367  addasssrg  7557  axaddass  7673