Theorem 3adant1r 1262

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

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

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  3adant2r  1264  3adant3r  1266  tfr1onlembacc  6607  tfr1onlembfn  6609  tfr1onlemaccex  6613  tfr1onlemres  6614  tfrcllembfn  6622  tfrcllemaccex  6626  tfrcllemres  6627  tfrcldm  6628  tfrcl  6629  mulassnqg  7745  prarloc  7864  prmuloc  7927  addasssrg  8117  axaddass  8233  ghmgrp  13904