Theorem ad4antr 483

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad5antr  485  tfr1onlemaccex  6199  tfrcllemaccex  6212  fimax2gtri  6748  en2eqpr  6754  unsnfidcex  6761  unsnfidcel  6762  ctssdc  6950  cauappcvgprlemloc  7408  caucvgprlemm  7424  caucvgprlemladdrl  7434  caucvgprlemlim  7437  caucvgprprlemml  7450  caucvgprprlemexbt  7462  caucvgprprlemlim  7467  caucvgsrlemgt1  7537  axcaucvglemres  7634  xaddval  9521  rebtwn2zlemstep  9923  hashunlem  10443  caucvgre  10645  cvg1nlemres  10649  resqrexlemglsq  10686  maxabslemval  10872  xrmaxiflemcl  10906  xrmaxifle  10907  xrmaxiflemab  10908  xrmaxiflemlub  10909  xrmaxiflemval  10911  xrmaxltsup  10919  divalglemeunn  11466  dvdsbnd  11493  bezoutlemnewy  11530  bezoutlemmain  11532  ctiunctlemfo  11795  txlm  12290  xmettx  12499  txmetcnp  12507  limcimo  12590  limccnp2cntop  12602