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  6557  tfrcllemaccex  6570  fimax2gtri  7134  en2eqpr  7142  unsnfidcex  7155  unsnfidcel  7156  ctssdc  7355  cauappcvgprlemloc  7915  caucvgprlemm  7931  caucvgprlemladdrl  7941  caucvgprlemlim  7944  caucvgprprlemml  7957  caucvgprprlemexbt  7969  caucvgprprlemlim  7974  suplocexprlemmu  7981  suplocexprlemloc  7984  suplocexprlemlub  7987  caucvgsrlemgt1  8058  suplocsrlemb  8069  suplocsrlem  8071  axcaucvglemres  8162  xaddval  10124  rebtwn2zlemstep  10558  nn0ltexp2  11017  hashunlem  11113  caucvgre  11604  cvg1nlemres  11608  resqrexlemglsq  11645  maxabslemval  11831  xrmaxiflemcl  11868  xrmaxifle  11869  xrmaxiflemab  11870  xrmaxiflemlub  11871  xrmaxiflemval  11873  xrmaxltsup  11881  divalglemeunn  12545  dvdsbnd  12590  bezoutlemnewy  12630  bezoutlemmain  12632  nninfctlemfo  12674  isprm5lem  12776  ctiunctlemfo  13123  prdsval  13419  sgrpidmndm  13566  mhmmnd  13766  mulgval  13772  txlm  15073  xmettx  15304  txmetcnp  15312  dedekindeu  15417  suplociccreex  15418  dedekindicclemlu  15424  dedekindicclemicc  15426  limcimo  15459  limccnp2cntop  15471  dvply2g  15560  lgsne0  15840  gfsumval  16792