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

Theorem adantll 453
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantll  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )

Proof of Theorem adantll
StepHypRef Expression
1 simpr 107 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 271 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad2antlr  466  ad2ant2l  485  ad2ant2lr  487  3ad2antl3  1079  3adant1l  1138  reu6  2753  sbc2iegf  2856  sbcralt  2862  sbcrext  2863  indifdir  3221  pofun  4077  poinxp  4437  ssimaex  5262  fndmdif  5300  dffo4  5343  foco2  5346  fcompt  5361  fconst2g  5404  foeqcnvco  5458  f1eqcocnv  5459  fliftel1  5462  isores3  5483  acexmid  5539  tfrlemi14d  5978  dom2lem  6283  ordiso2  6415  lt2addnq  6560  lt2mulnq  6561  ltexnqq  6564  genpdf  6664  addnqprl  6685  addnqpru  6686  addlocpr  6692  recexprlemopl  6781  caucvgsrlemgt1  6937  add4  7235  cnegex  7252  ltleadd  7515  zextle  8389  peano5uzti  8405  fnn0ind  8413  xrlttr  8817  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  fzaddel  9024  fzrev  9048  expivallem  9421  expival  9422  mulexp  9459  expadd  9462  expmul  9465  leexp1a  9475  bccl  9635  ovshftex  9648  2shfti  9660  caucvgre  9808  cvg1nlemcau  9811  resqrexlemcvg  9846  cau3lem  9941  climmpt  10052  subcn2  10063  climrecvg1n  10098  climcvg1nlem  10099  climcaucn  10101  dvdsext  10167  sqoddm1div8z  10198  bj-findis  10491
  Copyright terms: Public domain W3C validator