Theorem ad4antr 486

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad4antr	|- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

Proof of Theorem ad4antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	ad3antrrr 484	. 2 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )
3	2	adantr 274	1 |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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 is referenced by:  ad5antr  488  tfr1onlemaccex  6307  tfrcllemaccex  6320  fimax2gtri  6858  en2eqpr  6864  unsnfidcex  6876  unsnfidcel  6877  ctssdc  7069  cauappcvgprlemloc  7584  caucvgprlemm  7600  caucvgprlemladdrl  7610  caucvgprlemlim  7613  caucvgprprlemml  7626  caucvgprprlemexbt  7638  caucvgprprlemlim  7643  suplocexprlemmu  7650  suplocexprlemloc  7653  suplocexprlemlub  7656  caucvgsrlemgt1  7727  suplocsrlemb  7738  suplocsrlem  7740  axcaucvglemres  7831  xaddval  9772  rebtwn2zlemstep  10178  nn0ltexp2  10612  hashunlem  10706  caucvgre  10909  cvg1nlemres  10913  resqrexlemglsq  10950  maxabslemval  11136  xrmaxiflemcl  11172  xrmaxifle  11173  xrmaxiflemab  11174  xrmaxiflemlub  11175  xrmaxiflemval  11177  xrmaxltsup  11185  divalglemeunn  11843  dvdsbnd  11874  bezoutlemnewy  11914  bezoutlemmain  11916  ctiunctlemfo  12309  txlm  12820  xmettx  13051  txmetcnp  13059  dedekindeu  13142  suplociccreex  13143  dedekindicclemlu  13149  dedekindicclemicc  13151  limcimo  13175  limccnp2cntop  13187