Theorem ad4antr 498

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad5antr  500  tfr1onlemaccex  6623  tfrcllemaccex  6636  fimax2gtri  7210  en2eqpr  7218  unsnfidcex  7231  unsnfidcel  7232  fissfi  7267  ctssdc  7459  cauappcvgprlemloc  8025  caucvgprlemm  8041  caucvgprlemladdrl  8051  caucvgprlemlim  8054  caucvgprprlemml  8067  caucvgprprlemexbt  8079  caucvgprprlemlim  8084  suplocexprlemmu  8091  suplocexprlemloc  8094  suplocexprlemlub  8097  caucvgsrlemgt1  8168  suplocsrlemb  8179  suplocsrlem  8181  axcaucvglemres  8272  xaddval  10264  rebtwn2zlemstep  10704  nn0ltexp2  11169  hashunlem  11266  caucvgre  11769  cvg1nlemres  11773  resqrexlemglsq  11810  maxabslemval  11997  xrmaxiflemcl  12036  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemval  12041  xrmaxltsup  12049  divalglemeunn  12713  dvdsbnd  12758  bezoutlemnewy  12798  bezoutlemmain  12800  nninfctlemfo  12842  isprm5lem  12945  ctiunctlemfo  13388  sgrpidmndm  13792  mhmmnd  13978  mulgval  13984  gsumvalfi  14242  gsumzfi  14248  gsummptfidmsplit  14254  gsumresfi  14263  prdsval  14280  psrbaglefifi  15172  txlm  15505  xmettx  15736  txmetcnp  15744  dedekindeu  15849  suplociccreex  15850  dedekindicclemlu  15856  dedekindicclemicc  15858  limcimo  15891  limccnp2cntop  15903  dvply2g  15992  lgsne0  16362