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

Theorem ad5antr 496
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 494 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 276 1  |-  ( ( ( ( ( (
ph  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ps )
Colors of variables: wff set class
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:  ad6antr  498  difinfinf  7118  ctssdclemn0  7127  cauappcvgprlemladdfu  7671  caucvgprlemloc  7692  caucvgprlemladdfu  7694  caucvgprlemlim  7698  caucvgprprlemml  7711  caucvgprprlemloc  7720  caucvgprprlemlim  7728  suplocexprlemmu  7735  suplocexprlemru  7736  suplocexprlemloc  7738  suplocsrlem  7825  axcaucvglemres  7916  nn0ltexp2  10707  resqrexlemglsq  11049  xrmaxifle  11272  xrmaxiflemlub  11274  divalglemeuneg  11946  bezoutlemnewy  12015  ctiunctlemfo  12458  mhmmnd  13024  txmetcnp  14415  mulcncf  14488  suplociccreex  14499  cnplimclemr  14535  limccnpcntop  14541  lgsval  14802
  Copyright terms: Public domain W3C validator