Theorem ad4antr 494

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 492	. 2 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )
3	2	adantr 276	1 |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad5antr  496  tfr1onlemaccex  6434  tfrcllemaccex  6447  fimax2gtri  6998  en2eqpr  7004  unsnfidcex  7017  unsnfidcel  7018  ctssdc  7215  cauappcvgprlemloc  7765  caucvgprlemm  7781  caucvgprlemladdrl  7791  caucvgprlemlim  7794  caucvgprprlemml  7807  caucvgprprlemexbt  7819  caucvgprprlemlim  7824  suplocexprlemmu  7831  suplocexprlemloc  7834  suplocexprlemlub  7837  caucvgsrlemgt1  7908  suplocsrlemb  7919  suplocsrlem  7921  axcaucvglemres  8012  xaddval  9967  rebtwn2zlemstep  10395  nn0ltexp2  10854  hashunlem  10949  caucvgre  11292  cvg1nlemres  11296  resqrexlemglsq  11333  maxabslemval  11519  xrmaxiflemcl  11556  xrmaxifle  11557  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxiflemval  11561  xrmaxltsup  11569  divalglemeunn  12232  dvdsbnd  12277  bezoutlemnewy  12317  bezoutlemmain  12319  nninfctlemfo  12361  isprm5lem  12463  ctiunctlemfo  12810  prdsval  13105  sgrpidmndm  13252  mhmmnd  13452  mulgval  13458  txlm  14751  xmettx  14982  txmetcnp  14990  dedekindeu  15095  suplociccreex  15096  dedekindicclemlu  15102  dedekindicclemicc  15104  limcimo  15137  limccnp2cntop  15149  dvply2g  15238  lgsne0  15515