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

Theorem ad5antr 487
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 485 . 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  489  difinfinf  6986  ctssdclemn0  6995  cauappcvgprlemladdfu  7474  caucvgprlemloc  7495  caucvgprlemladdfu  7497  caucvgprlemlim  7501  caucvgprprlemml  7514  caucvgprprlemloc  7523  caucvgprprlemlim  7531  suplocexprlemmu  7538  suplocexprlemru  7539  suplocexprlemloc  7541  suplocsrlem  7628  axcaucvglemres  7719  resqrexlemglsq  10806  xrmaxifle  11027  xrmaxiflemlub  11029  divalglemeuneg  11631  bezoutlemnewy  11695  ctiunctlemfo  11963  txmetcnp  12701  mulcncf  12774  suplociccreex  12785  cnplimclemr  12821  limccnpcntop  12827
  Copyright terms: Public domain W3C validator