ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad5antr Unicode version

Theorem ad5antr 493
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad5antr  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )

Proof of Theorem ad5antr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad4antr 491 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 274 1  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad6antr  495  difinfinf  7074  ctssdclemn0  7083  cauappcvgprlemladdfu  7603  caucvgprlemloc  7624  caucvgprlemladdfu  7626  caucvgprlemlim  7630  caucvgprprlemml  7643  caucvgprprlemloc  7652  caucvgprprlemlim  7660  suplocexprlemmu  7667  suplocexprlemru  7668  suplocexprlemloc  7670  suplocsrlem  7757  axcaucvglemres  7848  nn0ltexp2  10631  resqrexlemglsq  10973  xrmaxifle  11196  xrmaxiflemlub  11198  divalglemeuneg  11869  bezoutlemnewy  11938  ctiunctlemfo  12381  txmetcnp  13271  mulcncf  13344  suplociccreex  13355  cnplimclemr  13391  limccnpcntop  13397  lgsval  13658
  Copyright terms: Public domain W3C validator