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

Theorem adantllr 478
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
adantllr  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )

Proof of Theorem adantllr
StepHypRef Expression
1 simpl 108 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 400 1  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )
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:  ad4ant13  510  ad4ant134  1212  r19.29an  2612  diffifi  6869  fimax2gtrilemstep  6875  cnegexlem3  8085  cnegex  8086  lemul12b  8766  climshftlemg  11254  prodeq2  11509  fprodmodd  11593  lcmdvds  12022  pw2dvdslemn  12108  tgcl  12819  metss  13249  ivthinclemlr  13370  ivthinclemur  13372
  Copyright terms: Public domain W3C validator