Theorem ad4antr 494

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  ad5antr  496  tfr1onlemaccex  6344  tfrcllemaccex  6357  fimax2gtri  6896  en2eqpr  6902  unsnfidcex  6914  unsnfidcel  6915  ctssdc  7107  cauappcvgprlemloc  7646  caucvgprlemm  7662  caucvgprlemladdrl  7672  caucvgprlemlim  7675  caucvgprprlemml  7688  caucvgprprlemexbt  7700  caucvgprprlemlim  7705  suplocexprlemmu  7712  suplocexprlemloc  7715  suplocexprlemlub  7718  caucvgsrlemgt1  7789  suplocsrlemb  7800  suplocsrlem  7802  axcaucvglemres  7893  xaddval  9839  rebtwn2zlemstep  10246  nn0ltexp2  10681  hashunlem  10775  caucvgre  10981  cvg1nlemres  10985  resqrexlemglsq  11022  maxabslemval  11208  xrmaxiflemcl  11244  xrmaxifle  11245  xrmaxiflemab  11246  xrmaxiflemlub  11247  xrmaxiflemval  11249  xrmaxltsup  11257  divalglemeunn  11916  dvdsbnd  11947  bezoutlemnewy  11987  bezoutlemmain  11989  isprm5lem  12131  ctiunctlemfo  12430  sgrpidmndm  12751  mhmmnd  12908  mulgval  12914  txlm  13561  xmettx  13792  txmetcnp  13800  dedekindeu  13883  suplociccreex  13884  dedekindicclemlu  13890  dedekindicclemicc  13892  limcimo  13916  limccnp2cntop  13928  lgsne0  14221