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  6557  tfrcllemaccex  6570  fimax2gtri  7134  en2eqpr  7142  unsnfidcex  7155  unsnfidcel  7156  ctssdc  7372  cauappcvgprlemloc  7932  caucvgprlemm  7948  caucvgprlemladdrl  7958  caucvgprlemlim  7961  caucvgprprlemml  7974  caucvgprprlemexbt  7986  caucvgprprlemlim  7991  suplocexprlemmu  7998  suplocexprlemloc  8001  suplocexprlemlub  8004  caucvgsrlemgt1  8075  suplocsrlemb  8086  suplocsrlem  8088  axcaucvglemres  8179  xaddval  10141  rebtwn2zlemstep  10575  nn0ltexp2  11034  hashunlem  11130  caucvgre  11621  cvg1nlemres  11625  resqrexlemglsq  11662  maxabslemval  11848  xrmaxiflemcl  11885  xrmaxifle  11886  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxiflemval  11890  xrmaxltsup  11898  divalglemeunn  12562  dvdsbnd  12607  bezoutlemnewy  12647  bezoutlemmain  12649  nninfctlemfo  12691  isprm5lem  12793  ctiunctlemfo  13140  prdsval  13436  sgrpidmndm  13583  mhmmnd  13783  mulgval  13789  txlm  15090  xmettx  15321  txmetcnp  15329  dedekindeu  15434  suplociccreex  15435  dedekindicclemlu  15441  dedekindicclemicc  15443  limcimo  15476  limccnp2cntop  15488  dvply2g  15577  lgsne0  15857  gfsumval  16809