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  3635  pofun  4040  ralxfrd  4160  rexxfrd  4161  poinxp  4352  relop  4429  fun11iun  5090  ssimaex  5177  fndmdif  5215  fconst2g  5319  foeqcnvco  5373  f1eqcocnv  5374  isocnv  5394  isocnv2  5395  riota2df  5431  grprinvd  5638  grpridd  5639  f1o2ndf1  5791  xpdom2  6241  mulcanpig  6319  prarloclemlt  6476  genpdf  6491  genpdisj  6506  addnqprl  6512  addnqpru  6513  addlocpr  6519  prmuloc  6547  mulnqprl  6549  mulnqpru  6550  mullocpr  6552  ltpopr  6569  ltsopr  6570  ltaddpr  6571  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  ltaprg  6592  recexprlemopu  6599  recexprlemloc  6603  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cnegexlem1  6983  cnegexlem3  6985  cnegex  6986  addsubeq4  7023  rimul  7369  divcanap6  7477  ltmul12a  7607  lemul12b  7608  zrevaddcl  8071  zextle  8107  fzind  8129  uz11  8271  qreccl  8351  qrevaddcl  8353  irradd  8355  xrlttr  8486  xrltso  8487  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  divelunit  8640  uzsubsubfz  8681  fzaddel  8692  fzrev  8716  elfzmlbp  8760  frec2uzrdg  8876  frecuzrdgfn  8879  frecuzrdgcl  8880  frecuzrdgsuc  8882  iseqovex  8899  iseqval  8900  iseqfveq2  8905  iseqfeq2  8906  expivallem  8910  expival  8911  expp1  8916  expnegap0  8917  expcllem  8920  mulexp  8948  expadd  8951  expaddzap  8953  expmulzap  8955  expdivap  8959  leexp1a  8963  expnlbnd  9026
  Copyright terms: Public domain W3C validator