Theorem ad4antr 485

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 483	. 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  487  tfr1onlemaccex  6245  tfrcllemaccex  6258  fimax2gtri  6795  en2eqpr  6801  unsnfidcex  6808  unsnfidcel  6809  ctssdc  6998  cauappcvgprlemloc  7460  caucvgprlemm  7476  caucvgprlemladdrl  7486  caucvgprlemlim  7489  caucvgprprlemml  7502  caucvgprprlemexbt  7514  caucvgprprlemlim  7519  suplocexprlemmu  7526  suplocexprlemloc  7529  suplocexprlemlub  7532  caucvgsrlemgt1  7603  suplocsrlemb  7614  suplocsrlem  7616  axcaucvglemres  7707  xaddval  9628  rebtwn2zlemstep  10030  hashunlem  10550  caucvgre  10753  cvg1nlemres  10757  resqrexlemglsq  10794  maxabslemval  10980  xrmaxiflemcl  11014  xrmaxifle  11015  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxiflemval  11019  xrmaxltsup  11027  divalglemeunn  11618  dvdsbnd  11645  bezoutlemnewy  11684  bezoutlemmain  11686  ctiunctlemfo  11952  txlm  12448  xmettx  12679  txmetcnp  12687  dedekindeu  12770  suplociccreex  12771  dedekindicclemlu  12777  dedekindicclemicc  12779  limcimo  12803  limccnp2cntop  12815