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  6475  genpdf  6490  genpdisj  6505  addnqprl  6511  addnqpru  6512  addlocpr  6518  prmuloc  6546  mulnqprl  6548  mulnqpru  6549  mullocpr  6551  ltpopr  6568  ltsopr  6569  ltaddpr  6570  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  ltaprg  6591  recexprlemopu  6598  recexprlemloc  6602  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cnegexlem1  6963  cnegexlem3  6965  cnegex  6966  addsubeq4  7003  rimul  7349  divcanap6  7457  ltmul12a  7587  lemul12b  7588  zrevaddcl  8051  zextle  8087  fzind  8109  uz11  8251  qreccl  8331  qrevaddcl  8333  irradd  8335  xrlttr  8466  xrltso  8467  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  divelunit  8620  uzsubsubfz  8661  fzaddel  8672  fzrev  8696  elfzmlbp  8740  frec2uzrdg  8856  frecuzrdgfn  8859  frecuzrdgcl  8860  frecuzrdgsuc  8862  iseqovex  8879  iseqval  8880  iseqfveq2  8885  iseqfeq2  8886  expivallem  8890  expival  8891  expp1  8896  expnegap0  8897  expcllem  8900  mulexp  8928  expadd  8931  expaddzap  8933  expmulzap  8935  expdivap  8939  leexp1a  8943  expnlbnd  9006
  Copyright terms: Public domain W3C validator