Theorem ad4antr 491

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad5antr  493  tfr1onlemaccex  6327  tfrcllemaccex  6340  fimax2gtri  6879  en2eqpr  6885  unsnfidcex  6897  unsnfidcel  6898  ctssdc  7090  cauappcvgprlemloc  7614  caucvgprlemm  7630  caucvgprlemladdrl  7640  caucvgprlemlim  7643  caucvgprprlemml  7656  caucvgprprlemexbt  7668  caucvgprprlemlim  7673  suplocexprlemmu  7680  suplocexprlemloc  7683  suplocexprlemlub  7686  caucvgsrlemgt1  7757  suplocsrlemb  7768  suplocsrlem  7770  axcaucvglemres  7861  xaddval  9802  rebtwn2zlemstep  10209  nn0ltexp2  10644  hashunlem  10739  caucvgre  10945  cvg1nlemres  10949  resqrexlemglsq  10986  maxabslemval  11172  xrmaxiflemcl  11208  xrmaxifle  11209  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxiflemval  11213  xrmaxltsup  11221  divalglemeunn  11880  dvdsbnd  11911  bezoutlemnewy  11951  bezoutlemmain  11953  isprm5lem  12095  ctiunctlemfo  12394  sgrpidmndm  12656  txlm  13073  xmettx  13304  txmetcnp  13312  dedekindeu  13395  suplociccreex  13396  dedekindicclemlu  13402  dedekindicclemicc  13404  limcimo  13428  limccnp2cntop  13440  lgsne0  13733