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  7078  ctssdclemn0  7087  cauappcvgprlemladdfu  7616  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlemlim  7643  caucvgprprlemml  7656  caucvgprprlemloc  7665  caucvgprprlemlim  7673  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemloc  7683  suplocsrlem  7770  axcaucvglemres  7861  nn0ltexp2  10644  resqrexlemglsq  10986  xrmaxifle  11209  xrmaxiflemlub  11211  divalglemeuneg  11882  bezoutlemnewy  11951  ctiunctlemfo  12394  txmetcnp  13312  mulcncf  13385  suplociccreex  13396  cnplimclemr  13432  limccnpcntop  13438  lgsval  13699
  Copyright terms: Public domain W3C validator