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  6509  tfrcllemaccex  6522  fimax2gtri  7084  en2eqpr  7092  unsnfidcex  7105  unsnfidcel  7106  ctssdc  7303  cauappcvgprlemloc  7862  caucvgprlemm  7878  caucvgprlemladdrl  7888  caucvgprlemlim  7891  caucvgprprlemml  7904  caucvgprprlemexbt  7916  caucvgprprlemlim  7921  suplocexprlemmu  7928  suplocexprlemloc  7931  suplocexprlemlub  7934  caucvgsrlemgt1  8005  suplocsrlemb  8016  suplocsrlem  8018  axcaucvglemres  8109  xaddval  10070  rebtwn2zlemstep  10502  nn0ltexp2  10961  hashunlem  11057  caucvgre  11532  cvg1nlemres  11536  resqrexlemglsq  11573  maxabslemval  11759  xrmaxiflemcl  11796  xrmaxifle  11797  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxiflemval  11801  xrmaxltsup  11809  divalglemeunn  12472  dvdsbnd  12517  bezoutlemnewy  12557  bezoutlemmain  12559  nninfctlemfo  12601  isprm5lem  12703  ctiunctlemfo  13050  prdsval  13346  sgrpidmndm  13493  mhmmnd  13693  mulgval  13699  txlm  14993  xmettx  15224  txmetcnp  15232  dedekindeu  15337  suplociccreex  15338  dedekindicclemlu  15344  dedekindicclemicc  15346  limcimo  15379  limccnp2cntop  15391  dvply2g  15480  lgsne0  15757