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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

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

This theorem is used by:  3adant2r  1264  3adant3r  1266  tfr1onlembacc  6618  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  tfrcl  6640  mulassnqg  7758  prarloc  7877  prmuloc  7940  addasssrg  8130  axaddass  8246  ghmgrp  13980