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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad5antr  500  tfr1onlemaccex  6619  tfrcllemaccex  6632  fimax2gtri  7206  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  fissfi  7263  ctssdc  7453  cauappcvgprlemloc  8019  caucvgprlemm  8035  caucvgprlemladdrl  8045  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemexbt  8073  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemloc  8088  suplocexprlemlub  8091  caucvgsrlemgt1  8162  suplocsrlemb  8173  suplocsrlem  8175  axcaucvglemres  8266  xaddval  10247  rebtwn2zlemstep  10687  nn0ltexp2  11147  hashunlem  11244  caucvgre  11747  cvg1nlemres  11751  resqrexlemglsq  11788  maxabslemval  11974  xrmaxiflemcl  12011  xrmaxifle  12012  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxiflemval  12016  xrmaxltsup  12024  divalglemeunn  12688  dvdsbnd  12733  bezoutlemnewy  12773  bezoutlemmain  12775  nninfctlemfo  12817  isprm5lem  12919  ctiunctlemfo  13330  sgrpidmndm  13733  mhmmnd  13919  mulgval  13925  gsumvalfi  14152  gsumzfi  14158  prdsval  14173  txlm  15380  xmettx  15611  txmetcnp  15619  dedekindeu  15724  suplociccreex  15725  dedekindicclemlu  15731  dedekindicclemicc  15733  limcimo  15766  limccnp2cntop  15778  dvply2g  15867  lgsne0  16157