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  6513  tfrcllemaccex  6526  fimax2gtri  7090  en2eqpr  7098  unsnfidcex  7111  unsnfidcel  7112  ctssdc  7311  cauappcvgprlemloc  7871  caucvgprlemm  7887  caucvgprlemladdrl  7897  caucvgprlemlim  7900  caucvgprprlemml  7913  caucvgprprlemexbt  7925  caucvgprprlemlim  7930  suplocexprlemmu  7937  suplocexprlemloc  7940  suplocexprlemlub  7943  caucvgsrlemgt1  8014  suplocsrlemb  8025  suplocsrlem  8027  axcaucvglemres  8118  xaddval  10079  rebtwn2zlemstep  10511  nn0ltexp2  10970  hashunlem  11066  caucvgre  11541  cvg1nlemres  11545  resqrexlemglsq  11582  maxabslemval  11768  xrmaxiflemcl  11805  xrmaxifle  11806  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxiflemval  11810  xrmaxltsup  11818  divalglemeunn  12481  dvdsbnd  12526  bezoutlemnewy  12566  bezoutlemmain  12568  nninfctlemfo  12610  isprm5lem  12712  ctiunctlemfo  13059  prdsval  13355  sgrpidmndm  13502  mhmmnd  13702  mulgval  13708  txlm  15002  xmettx  15233  txmetcnp  15241  dedekindeu  15346  suplociccreex  15347  dedekindicclemlu  15353  dedekindicclemicc  15355  limcimo  15388  limccnp2cntop  15400  dvply2g  15489  lgsne0  15766  gfsumval  16680