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  6316  tfrcllemaccex  6329  fimax2gtri  6867  en2eqpr  6873  unsnfidcex  6885  unsnfidcel  6886  ctssdc  7078  cauappcvgprlemloc  7593  caucvgprlemm  7609  caucvgprlemladdrl  7619  caucvgprlemlim  7622  caucvgprprlemml  7635  caucvgprprlemexbt  7647  caucvgprprlemlim  7652  suplocexprlemmu  7659  suplocexprlemloc  7662  suplocexprlemlub  7665  caucvgsrlemgt1  7736  suplocsrlemb  7747  suplocsrlem  7749  axcaucvglemres  7840  xaddval  9781  rebtwn2zlemstep  10188  nn0ltexp2  10623  hashunlem  10717  caucvgre  10923  cvg1nlemres  10927  resqrexlemglsq  10964  maxabslemval  11150  xrmaxiflemcl  11186  xrmaxifle  11187  xrmaxiflemab  11188  xrmaxiflemlub  11189  xrmaxiflemval  11191  xrmaxltsup  11199  divalglemeunn  11858  dvdsbnd  11889  bezoutlemnewy  11929  bezoutlemmain  11931  isprm5lem  12073  ctiunctlemfo  12372  txlm  12929  xmettx  13160  txmetcnp  13168  dedekindeu  13251  suplociccreex  13252  dedekindicclemlu  13258  dedekindicclemicc  13260  limcimo  13284  limccnp2cntop  13296  lgsne0  13589