Theorem 3adant3r 1230

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
3adant3r	|- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )

Proof of Theorem 3adant3r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3com13 1203	. . 3 |- ( ( ch /\ ps /\ ph ) -> th )
3	2	3adant1r 1226	. 2 |- ( ( ( ch /\ ta ) /\ ps /\ ph ) -> th )
4	3	3com13 1203	1 |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )

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

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 975

This theorem is referenced by:  addassnqg  7344  mulassnqg  7346  prarloc  7465  ltpopr  7557  ltexprlemfl  7571  ltexprlemfu  7573  addasssrg  7718  axaddass  7834  apmul1  8705  ltmul2  8772  lemul2  8773  dvdscmulr  11782  dvdsmulcr  11783  modremain  11888  ndvdsadd  11890  rpexp12i  12109  xblcntrps  13207  xblcntr  13208