Theorem 3adant1r 1257

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

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

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 1006

This theorem is referenced by:  3adant2r  1259  3adant3r  1261  tfr1onlembacc  6511  tfr1onlembfn  6513  tfr1onlemaccex  6517  tfr1onlemres  6518  tfrcllembfn  6526  tfrcllemaccex  6530  tfrcllemres  6531  tfrcldm  6532  tfrcl  6533  mulassnqg  7607  prarloc  7726  prmuloc  7789  addasssrg  7979  axaddass  8095  ghmgrp  13726