Theorem ad4antr 498

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 496	. 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  500  tfr1onlemaccex  6609  tfrcllemaccex  6622  fimax2gtri  7196  en2eqpr  7204  unsnfidcex  7217  unsnfidcel  7218  fissfi  7253  ctssdc  7443  cauappcvgprlemloc  8009  caucvgprlemm  8025  caucvgprlemladdrl  8035  caucvgprlemlim  8038  caucvgprprlemml  8051  caucvgprprlemexbt  8063  caucvgprprlemlim  8068  suplocexprlemmu  8075  suplocexprlemloc  8078  suplocexprlemlub  8081  caucvgsrlemgt1  8152  suplocsrlemb  8163  suplocsrlem  8165  axcaucvglemres  8256  xaddval  10226  rebtwn2zlemstep  10665  nn0ltexp2  11125  hashunlem  11222  caucvgre  11725  cvg1nlemres  11729  resqrexlemglsq  11766  maxabslemval  11952  xrmaxiflemcl  11989  xrmaxifle  11990  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxiflemval  11994  xrmaxltsup  12002  divalglemeunn  12666  dvdsbnd  12711  bezoutlemnewy  12751  bezoutlemmain  12753  nninfctlemfo  12795  isprm5lem  12897  ctiunctlemfo  13308  sgrpidmndm  13710  mhmmnd  13896  mulgval  13902  gsumvalfi  14129  gsumzfi  14135  prdsval  14150  txlm  15303  xmettx  15534  txmetcnp  15542  dedekindeu  15647  suplociccreex  15648  dedekindicclemlu  15654  dedekindicclemicc  15656  limcimo  15689  limccnp2cntop  15701  dvply2g  15790  lgsne0  16071