ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantlr Structured version   GIF version

Theorem adantlr 446
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 ((φ ψ) → χ)
Assertion
Ref Expression
adantlr (((φ θ) ψ) → χ)

Proof of Theorem adantlr
StepHypRef Expression
1 simpl 102 . 2 ((φ θ) → φ)
2 adant2.1 . 2 ((φ ψ) → χ)
31, 2sylan 267 1 (((φ θ) ψ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad2antrr  457  ad2ant2r  478  ad2ant2rl  480  3ad2antl1  1065  3ad2antl2  1066  3adant1r  1127  bilukdc  1284  intab  3634  pofun  4039  ralxfrd  4159  rexxfrd  4160  poinxp  4351  relop  4428  fun11iun  5088  ssimaex  5175  fndmdif  5213  fconst2g  5317  foeqcnvco  5371  f1eqcocnv  5372  isocnv  5392  isocnv2  5393  riota2df  5428  grprinvd  5635  grpridd  5636  f1o2ndf1  5788  xpdom2  6234  mulcanpig  6312  prarloclemlt  6468  genpdf  6483  genpdisj  6499  addnqprl  6505  addnqpru  6506  addlocpr  6512  prmuloc  6537  mulnqprl  6539  mulnqpru  6540  mullocpr  6542  ltpopr  6559  ltsopr  6560  ltaddpr  6561  ltexprlemdisj  6570  ltexprlemloc  6571  ltexprlemru  6576  addcanprleml  6578  addcanprlemu  6579  ltaprg  6582  recexprlemopu  6589  recexprlemloc  6593  cnegexlem1  6935  cnegexlem3  6937  cnegex  6938  addsubeq4  6975  rimul  7321  divcanap6  7429  ltmul12a  7558  lemul12b  7559  zrevaddcl  8021  zextle  8056  fzind  8078  uz11  8220  qreccl  8300  qrevaddcl  8302  irradd  8304  xrlttr  8434  xrltso  8435  iccshftr  8580  iccshftl  8582  iccdil  8584  icccntr  8586  divelunit  8588  uzsubsubfz  8627  fzaddel  8638  fzrev  8662  elfzmlbp  8706
  Copyright terms: Public domain W3C validator