Theorem 3adant3r 1213

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

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

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 964

This theorem is referenced by:  addassnqg  7190  mulassnqg  7192  prarloc  7311  ltpopr  7403  ltexprlemfl  7417  ltexprlemfu  7419  addasssrg  7564  axaddass  7680  apmul1  8548  ltmul2  8614  lemul2  8615  dvdscmulr  11522  dvdsmulcr  11523  modremain  11626  ndvdsadd  11628  rpexp12i  11833  xblcntrps  12582  xblcntr  12583