Theorem 3adant1r 1210

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

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

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 965

This theorem is referenced by:  3adant2r  1212  3adant3r  1214  tfr1onlembacc  6247  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcllemres  6267  tfrcldm  6268  tfrcl  6269  mulassnqg  7216  prarloc  7335  prmuloc  7398  addasssrg  7588  axaddass  7704