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

Theorem adantllr 481
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 109 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 402 1  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )
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:  ad4ant13  513  ad4ant134  1219  ad5ant145  1246  r19.29an  2632  diffifi  6923  fimax2gtrilemstep  6929  cnegexlem3  8165  cnegex  8166  lemul12b  8849  climshftlemg  11345  prodeq2  11600  fprodmodd  11684  lcmdvds  12114  pw2dvdslemn  12200  dfgrp3mlem  13057  tgcl  14041  metss  14471  ivthinclemlr  14592  ivthinclemur  14594
  Copyright terms: Public domain W3C validator