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

Theorem adantll 467
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 109 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 281 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
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:  ad2antlr  480  ad2ant2l  499  ad2ant2lr  501  ad5ant23  513  ad5ant24  514  ad5ant25  515  3ad2antl3  1145  3adant1l  1208  reu6  2873  sbc2iegf  2979  sbcralt  2985  sbcrext  2986  indifdir  3332  pofun  4237  poinxp  4611  ssimaex  5485  fndmdif  5528  dffo4  5571  fcompt  5593  fconst2g  5638  foco2  5658  foeqcnvco  5694  f1eqcocnv  5695  fliftel1  5698  isores3  5719  acexmid  5776  tfrlemi14d  6233  tfrcl  6264  dom2lem  6669  fiintim  6820  ordiso2  6923  mkvprop  7035  lt2addnq  7231  lt2mulnq  7232  ltexnqq  7235  genpdf  7335  addnqprl  7356  addnqpru  7357  addlocpr  7363  recexprlemopl  7452  caucvgsrlemgt1  7622  add4  7942  cnegex  7959  ltleadd  8227  zextle  9161  peano5uzti  9178  fnn0ind  9186  xrlttr  9604  xaddass  9675  iccshftr  9800  iccshftl  9802  iccdil  9804  icccntr  9806  fzaddel  9863  fzrev  9888  exbtwnzlemshrink  10050  seq3val  10255  iseqf1olemab  10286  exp3vallem  10318  mulexp  10356  expadd  10359  expmul  10362  leexp1a  10372  bccl  10537  hashfacen  10603  ovshftex  10615  2shfti  10627  caucvgre  10777  cvg1nlemcau  10780  resqrexlemcvg  10815  cau3lem  10910  rexico  11017  iooinsup  11070  climmpt  11093  subcn2  11104  climrecvg1n  11141  climcvg1nlem  11142  climcaucn  11144  mertenslem2  11329  eftlcl  11418  reeftlcl  11419  dvdsext  11576  sqoddm1div8z  11606  bezoutlemaz  11714  bezoutr1  11744  dvdslcm  11773  lcmeq0  11775  lcmcl  11776  lcmneg  11778  lcmdvds  11783  coprmgcdb  11792  dvdsprime  11826  cnco  12416  cnss1  12421  tx2cn  12465  upxp  12467  metss  12689  txmetcnp  12713  cncfss  12765  cosz12  12895  bj-findis  13321
  Copyright terms: Public domain W3C validator