Theorem 3adant3r 1225

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 1198	. . 3 |- ( ( ch /\ ps /\ ph ) -> th )
3	2	3adant1r 1221	. 2 |- ( ( ( ch /\ ta ) /\ ps /\ ph ) -> th )
4	3	3com13 1198	1 |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )

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

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 970

This theorem is referenced by:  addassnqg  7323  mulassnqg  7325  prarloc  7444  ltpopr  7536  ltexprlemfl  7550  ltexprlemfu  7552  addasssrg  7697  axaddass  7813  apmul1  8684  ltmul2  8751  lemul2  8752  dvdscmulr  11760  dvdsmulcr  11761  modremain  11866  ndvdsadd  11868  rpexp12i  12087  xblcntrps  13053  xblcntr  13054