Theorem ad4antr 477

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  ad5antr  479  en2eqpr  6380  unsnfidcex  6385  unsnfidcel  6386  cauappcvgprlemloc  6842  caucvgprlemm  6858  caucvgprlemladdrl  6868  caucvgprlemlim  6871  caucvgprprlemml  6884  caucvgprprlemexbt  6896  caucvgprprlemlim  6901  caucvgsrlemgt1  6971  axcaucvglemres  7065  rebtwn2zlemstep  9261  caucvgre  9867  cvg1nlemres  9871  resqrexlemglsq  9908  maxabslemval  10094  divalglemeunn  10321  dvdsbnd  10348  bezoutlemnewy  10385  bezoutlemmain  10387