Theorem ad4antr 498

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 496	. 2 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )
3	2	adantr 276	1 |- ( ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) /\ et ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad5antr  500  tfr1onlemaccex  6619  tfrcllemaccex  6632  fimax2gtri  7206  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  fissfi  7263  ctssdc  7453  cauappcvgprlemloc  8019  caucvgprlemm  8035  caucvgprlemladdrl  8045  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemexbt  8073  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemloc  8088  suplocexprlemlub  8091  caucvgsrlemgt1  8162  suplocsrlemb  8173  suplocsrlem  8175  axcaucvglemres  8266  xaddval  10257  rebtwn2zlemstep  10697  nn0ltexp2  11161  hashunlem  11258  caucvgre  11761  cvg1nlemres  11765  resqrexlemglsq  11802  maxabslemval  11989  xrmaxiflemcl  12027  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemval  12032  xrmaxltsup  12040  divalglemeunn  12704  dvdsbnd  12749  bezoutlemnewy  12789  bezoutlemmain  12791  nninfctlemfo  12833  isprm5lem  12936  ctiunctlemfo  13379  sgrpidmndm  13782  mhmmnd  13968  mulgval  13974  gsumvalfi  14201  gsumzfi  14207  prdsval  14222  txlm  15429  xmettx  15660  txmetcnp  15668  dedekindeu  15773  suplociccreex  15774  dedekindicclemlu  15780  dedekindicclemicc  15782  limcimo  15815  limccnp2cntop  15827  dvply2g  15916  lgsne0  16255