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  6624  tfrcllemaccex  6637  fimax2gtri  7212  en2eqpr  7220  unsnfidcex  7233  unsnfidcel  7234  fissfi  7269  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  10263  rebtwn2zlemstep  10703  nn0ltexp2  11168  hashunlem  11265  caucvgre  11768  cvg1nlemres  11772  resqrexlemglsq  11809  maxabslemval  11996  xrmaxiflemcl  12035  xrmaxifle  12036  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxiflemval  12040  xrmaxltsup  12048  divalglemeunn  12712  dvdsbnd  12757  bezoutlemnewy  12797  bezoutlemmain  12799  nninfctlemfo  12841  isprm5lem  12944  ctiunctlemfo  13387  sgrpidmndm  13791  mhmmnd  13977  mulgval  13983  gsumvalfi  14241  gsumzfi  14247  gsummptfidmsplit  14253  gsumresfi  14262  prdsval  14279  psrbaglefifi  15175  txlm  15522  xmettx  15753  txmetcnp  15761  dedekindeu  15866  suplociccreex  15867  dedekindicclemlu  15873  dedekindicclemicc  15875  limcimo  15908  limccnp2cntop  15920  dvply2g  16009  lgsne0  16379