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  6401  tfrcllemaccex  6414  fimax2gtri  6957  en2eqpr  6963  unsnfidcex  6976  unsnfidcel  6977  ctssdc  7172  cauappcvgprlemloc  7712  caucvgprlemm  7728  caucvgprlemladdrl  7738  caucvgprlemlim  7741  caucvgprprlemml  7754  caucvgprprlemexbt  7766  caucvgprprlemlim  7771  suplocexprlemmu  7778  suplocexprlemloc  7781  suplocexprlemlub  7784  caucvgsrlemgt1  7855  suplocsrlemb  7866  suplocsrlem  7868  axcaucvglemres  7959  xaddval  9911  rebtwn2zlemstep  10321  nn0ltexp2  10780  hashunlem  10875  caucvgre  11125  cvg1nlemres  11129  resqrexlemglsq  11166  maxabslemval  11352  xrmaxiflemcl  11388  xrmaxifle  11389  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxiflemval  11393  xrmaxltsup  11401  divalglemeunn  12062  dvdsbnd  12093  bezoutlemnewy  12133  bezoutlemmain  12135  nninfctlemfo  12177  isprm5lem  12279  ctiunctlemfo  12596  sgrpidmndm  13001  mhmmnd  13186  mulgval  13192  txlm  14447  xmettx  14678  txmetcnp  14686  dedekindeu  14777  suplociccreex  14778  dedekindicclemlu  14784  dedekindicclemicc  14786  limcimo  14819  limccnp2cntop  14831  lgsne0  15154