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  6349  tfrcllemaccex  6362  fimax2gtri  6901  en2eqpr  6907  unsnfidcex  6919  unsnfidcel  6920  ctssdc  7112  cauappcvgprlemloc  7651  caucvgprlemm  7667  caucvgprlemladdrl  7677  caucvgprlemlim  7680  caucvgprprlemml  7693  caucvgprprlemexbt  7705  caucvgprprlemlim  7710  suplocexprlemmu  7717  suplocexprlemloc  7720  suplocexprlemlub  7723  caucvgsrlemgt1  7794  suplocsrlemb  7805  suplocsrlem  7807  axcaucvglemres  7898  xaddval  9845  rebtwn2zlemstep  10253  nn0ltexp2  10689  hashunlem  10784  caucvgre  10990  cvg1nlemres  10994  resqrexlemglsq  11031  maxabslemval  11217  xrmaxiflemcl  11253  xrmaxifle  11254  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxiflemval  11258  xrmaxltsup  11266  divalglemeunn  11926  dvdsbnd  11957  bezoutlemnewy  11997  bezoutlemmain  11999  isprm5lem  12141  ctiunctlemfo  12440  sgrpidmndm  12821  mhmmnd  12980  mulgval  12986  txlm  13782  xmettx  14013  txmetcnp  14021  dedekindeu  14104  suplociccreex  14105  dedekindicclemlu  14111  dedekindicclemicc  14113  limcimo  14137  limccnp2cntop  14149  lgsne0  14442