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

Theorem ad5antr 483
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 481 . 2  |-  ( ( ( ( ( ph  /\ 
ch )  /\  th )  /\  ta )  /\  et )  ->  ps )
32adantr 272 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad6antr  485  difinfinf  6901  ctssdclemn0  6910  cauappcvgprlemladdfu  7363  caucvgprlemloc  7384  caucvgprlemladdfu  7386  caucvgprlemlim  7390  caucvgprprlemml  7403  caucvgprprlemloc  7412  caucvgprprlemlim  7420  axcaucvglemres  7584  resqrexlemglsq  10634  xrmaxifle  10854  xrmaxiflemlub  10856  divalglemeuneg  11415  bezoutlemnewy  11477  mulcncf  12503  limccnpcntop  12520
  Copyright terms: Public domain W3C validator