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  6436  tfrcllemaccex  6449  fimax2gtri  7000  en2eqpr  7006  unsnfidcex  7019  unsnfidcel  7020  ctssdc  7217  cauappcvgprlemloc  7767  caucvgprlemm  7783  caucvgprlemladdrl  7793  caucvgprlemlim  7796  caucvgprprlemml  7809  caucvgprprlemexbt  7821  caucvgprprlemlim  7826  suplocexprlemmu  7833  suplocexprlemloc  7836  suplocexprlemlub  7839  caucvgsrlemgt1  7910  suplocsrlemb  7921  suplocsrlem  7923  axcaucvglemres  8014  xaddval  9969  rebtwn2zlemstep  10397  nn0ltexp2  10856  hashunlem  10951  caucvgre  11325  cvg1nlemres  11329  resqrexlemglsq  11366  maxabslemval  11552  xrmaxiflemcl  11589  xrmaxifle  11590  xrmaxiflemab  11591  xrmaxiflemlub  11592  xrmaxiflemval  11594  xrmaxltsup  11602  divalglemeunn  12265  dvdsbnd  12310  bezoutlemnewy  12350  bezoutlemmain  12352  nninfctlemfo  12394  isprm5lem  12496  ctiunctlemfo  12843  prdsval  13138  sgrpidmndm  13285  mhmmnd  13485  mulgval  13491  txlm  14784  xmettx  15015  txmetcnp  15023  dedekindeu  15128  suplociccreex  15129  dedekindicclemlu  15135  dedekindicclemicc  15137  limcimo  15170  limccnp2cntop  15182  dvply2g  15271  lgsne0  15548