Theorem ad4antr 478

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 476	. 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  480  tfr1onlemaccex  6067  tfrcllemaccex  6080  fimax2gtri  6569  en2eqpr  6575  unsnfidcex  6582  unsnfidcel  6583  cauappcvgprlemloc  7155  caucvgprlemm  7171  caucvgprlemladdrl  7181  caucvgprlemlim  7184  caucvgprprlemml  7197  caucvgprprlemexbt  7209  caucvgprprlemlim  7214  caucvgsrlemgt1  7284  axcaucvglemres  7378  rebtwn2zlemstep  9592  hashunlem  10108  caucvgre  10309  cvg1nlemres  10313  resqrexlemglsq  10350  maxabslemval  10536  divalglemeunn  10796  dvdsbnd  10823  bezoutlemnewy  10860  bezoutlemmain  10862