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  6500  tfrcllemaccex  6513  fimax2gtri  7072  en2eqpr  7080  unsnfidcex  7093  unsnfidcel  7094  ctssdc  7291  cauappcvgprlemloc  7850  caucvgprlemm  7866  caucvgprlemladdrl  7876  caucvgprlemlim  7879  caucvgprprlemml  7892  caucvgprprlemexbt  7904  caucvgprprlemlim  7909  suplocexprlemmu  7916  suplocexprlemloc  7919  suplocexprlemlub  7922  caucvgsrlemgt1  7993  suplocsrlemb  8004  suplocsrlem  8006  axcaucvglemres  8097  xaddval  10053  rebtwn2zlemstep  10484  nn0ltexp2  10943  hashunlem  11038  caucvgre  11508  cvg1nlemres  11512  resqrexlemglsq  11549  maxabslemval  11735  xrmaxiflemcl  11772  xrmaxifle  11773  xrmaxiflemab  11774  xrmaxiflemlub  11775  xrmaxiflemval  11777  xrmaxltsup  11785  divalglemeunn  12448  dvdsbnd  12493  bezoutlemnewy  12533  bezoutlemmain  12535  nninfctlemfo  12577  isprm5lem  12679  ctiunctlemfo  13026  prdsval  13322  sgrpidmndm  13469  mhmmnd  13669  mulgval  13675  txlm  14969  xmettx  15200  txmetcnp  15208  dedekindeu  15313  suplociccreex  15314  dedekindicclemlu  15320  dedekindicclemicc  15322  limcimo  15355  limccnp2cntop  15367  dvply2g  15456  lgsne0  15733