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  3ad2antl3  1130  3adant1l  1193  reu6  2846  sbc2iegf  2951  sbcralt  2957  sbcrext  2958  indifdir  3302  pofun  4204  poinxp  4578  ssimaex  5450  fndmdif  5493  dffo4  5536  fcompt  5558  fconst2g  5603  foco2  5623  foeqcnvco  5659  f1eqcocnv  5660  fliftel1  5663  isores3  5684  acexmid  5741  tfrlemi14d  6198  tfrcl  6229  dom2lem  6634  fiintim  6785  ordiso2  6888  mkvprop  7000  lt2addnq  7180  lt2mulnq  7181  ltexnqq  7184  genpdf  7284  addnqprl  7305  addnqpru  7306  addlocpr  7312  recexprlemopl  7401  caucvgsrlemgt1  7571  add4  7891  cnegex  7908  ltleadd  8176  zextle  9110  peano5uzti  9127  fnn0ind  9135  xrlttr  9549  xaddass  9620  iccshftr  9745  iccshftl  9747  iccdil  9749  icccntr  9751  fzaddel  9807  fzrev  9832  exbtwnzlemshrink  9994  seq3val  10199  iseqf1olemab  10230  exp3vallem  10262  mulexp  10300  expadd  10303  expmul  10306  leexp1a  10316  bccl  10481  hashfacen  10547  ovshftex  10559  2shfti  10571  caucvgre  10721  cvg1nlemcau  10724  resqrexlemcvg  10759  cau3lem  10854  rexico  10961  iooinsup  11014  climmpt  11037  subcn2  11048  climrecvg1n  11085  climcvg1nlem  11086  climcaucn  11088  mertenslem2  11273  eftlcl  11321  reeftlcl  11322  dvdsext  11480  sqoddm1div8z  11510  bezoutlemaz  11618  bezoutr1  11648  dvdslcm  11677  lcmeq0  11679  lcmcl  11680  lcmneg  11682  lcmdvds  11687  coprmgcdb  11696  dvdsprime  11730  cnco  12317  cnss1  12322  tx2cn  12366  upxp  12368  metss  12590  txmetcnp  12614  cncfss  12666  cosz12  12788  bj-findis  13104
  Copyright terms: Public domain W3C validator