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  6346  tfrcllemaccex  6359  fimax2gtri  6898  en2eqpr  6904  unsnfidcex  6916  unsnfidcel  6917  ctssdc  7109  cauappcvgprlemloc  7648  caucvgprlemm  7664  caucvgprlemladdrl  7674  caucvgprlemlim  7677  caucvgprprlemml  7690  caucvgprprlemexbt  7702  caucvgprprlemlim  7707  suplocexprlemmu  7714  suplocexprlemloc  7717  suplocexprlemlub  7720  caucvgsrlemgt1  7791  suplocsrlemb  7802  suplocsrlem  7804  axcaucvglemres  7895  xaddval  9841  rebtwn2zlemstep  10248  nn0ltexp2  10683  hashunlem  10777  caucvgre  10983  cvg1nlemres  10987  resqrexlemglsq  11024  maxabslemval  11210  xrmaxiflemcl  11246  xrmaxifle  11247  xrmaxiflemab  11248  xrmaxiflemlub  11249  xrmaxiflemval  11251  xrmaxltsup  11259  divalglemeunn  11918  dvdsbnd  11949  bezoutlemnewy  11989  bezoutlemmain  11991  isprm5lem  12133  ctiunctlemfo  12432  sgrpidmndm  12753  mhmmnd  12912  mulgval  12918  txlm  13650  xmettx  13881  txmetcnp  13889  dedekindeu  13972  suplociccreex  13973  dedekindicclemlu  13979  dedekindicclemicc  13981  limcimo  14005  limccnp2cntop  14017  lgsne0  14310