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  7454  cauappcvgprlemloc  8020  caucvgprlemm  8036  caucvgprlemladdrl  8046  caucvgprlemlim  8049  caucvgprprlemml  8062  caucvgprprlemexbt  8074  caucvgprprlemlim  8079  suplocexprlemmu  8086  suplocexprlemloc  8089  suplocexprlemlub  8092  caucvgsrlemgt1  8163  suplocsrlemb  8174  suplocsrlem  8176  axcaucvglemres  8267  xaddval  10258  rebtwn2zlemstep  10698  nn0ltexp2  11163  hashunlem  11260  caucvgre  11763  cvg1nlemres  11767  resqrexlemglsq  11804  maxabslemval  11991  xrmaxiflemcl  12030  xrmaxifle  12031  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxiflemval  12035  xrmaxltsup  12043  divalglemeunn  12707  dvdsbnd  12752  bezoutlemnewy  12792  bezoutlemmain  12794  nninfctlemfo  12836  isprm5lem  12939  ctiunctlemfo  13382  sgrpidmndm  13786  mhmmnd  13972  mulgval  13978  gsumvalfi  14236  gsumzfi  14242  prdsval  14257  psrbaglefifi  15147  txlm  15471  xmettx  15702  txmetcnp  15710  dedekindeu  15815  suplociccreex  15816  dedekindicclemlu  15822  dedekindicclemicc  15824  limcimo  15857  limccnp2cntop  15869  dvply2g  15958  lgsne0  16323