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  6617  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  tfrcl  6639  mulassnqg  7758  prarloc  7877  prmuloc  7940  addasssrg  8130  axaddass  8246  ghmgrp  13981