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  6514  tfrcllemaccex  6527  fimax2gtri  7091  en2eqpr  7099  unsnfidcex  7112  unsnfidcel  7113  ctssdc  7312  cauappcvgprlemloc  7872  caucvgprlemm  7888  caucvgprlemladdrl  7898  caucvgprlemlim  7901  caucvgprprlemml  7914  caucvgprprlemexbt  7926  caucvgprprlemlim  7931  suplocexprlemmu  7938  suplocexprlemloc  7941  suplocexprlemlub  7944  caucvgsrlemgt1  8015  suplocsrlemb  8026  suplocsrlem  8028  axcaucvglemres  8119  xaddval  10080  rebtwn2zlemstep  10513  nn0ltexp2  10972  hashunlem  11068  caucvgre  11559  cvg1nlemres  11563  resqrexlemglsq  11600  maxabslemval  11786  xrmaxiflemcl  11823  xrmaxifle  11824  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxiflemval  11828  xrmaxltsup  11836  divalglemeunn  12500  dvdsbnd  12545  bezoutlemnewy  12585  bezoutlemmain  12587  nninfctlemfo  12629  isprm5lem  12731  ctiunctlemfo  13078  prdsval  13374  sgrpidmndm  13521  mhmmnd  13721  mulgval  13727  txlm  15022  xmettx  15253  txmetcnp  15261  dedekindeu  15366  suplociccreex  15367  dedekindicclemlu  15373  dedekindicclemicc  15375  limcimo  15408  limccnp2cntop  15420  dvply2g  15509  lgsne0  15786  gfsumval  16732