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  6494  tfrcllemaccex  6507  fimax2gtri  7063  en2eqpr  7069  unsnfidcex  7082  unsnfidcel  7083  ctssdc  7280  cauappcvgprlemloc  7839  caucvgprlemm  7855  caucvgprlemladdrl  7865  caucvgprlemlim  7868  caucvgprprlemml  7881  caucvgprprlemexbt  7893  caucvgprprlemlim  7898  suplocexprlemmu  7905  suplocexprlemloc  7908  suplocexprlemlub  7911  caucvgsrlemgt1  7982  suplocsrlemb  7993  suplocsrlem  7995  axcaucvglemres  8086  xaddval  10041  rebtwn2zlemstep  10472  nn0ltexp2  10931  hashunlem  11026  caucvgre  11492  cvg1nlemres  11496  resqrexlemglsq  11533  maxabslemval  11719  xrmaxiflemcl  11756  xrmaxifle  11757  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxiflemval  11761  xrmaxltsup  11769  divalglemeunn  12432  dvdsbnd  12477  bezoutlemnewy  12517  bezoutlemmain  12519  nninfctlemfo  12561  isprm5lem  12663  ctiunctlemfo  13010  prdsval  13306  sgrpidmndm  13453  mhmmnd  13653  mulgval  13659  txlm  14953  xmettx  15184  txmetcnp  15192  dedekindeu  15297  suplociccreex  15298  dedekindicclemlu  15304  dedekindicclemicc  15306  limcimo  15339  limccnp2cntop  15351  dvply2g  15440  lgsne0  15717