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

Theorem adantll 445
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
adantll (((θ φ) ψ) → χ)

Proof of Theorem adantll
StepHypRef Expression
1 simpr 103 . 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:  ad2antlr  458  ad2ant2l  477  ad2ant2lr  479  3ad2antl3  1067  3adant1l  1126  reu6  2724  sbc2iegf  2822  sbcralt  2828  sbcrext  2829  indifdir  3187  pofun  4040  poinxp  4352  ssimaex  5177  fndmdif  5215  dffo4  5258  foco2  5261  fcompt  5276  fconst2g  5319  foeqcnvco  5373  f1eqcocnv  5374  fliftel1  5377  isores3  5398  acexmid  5454  tfrlemi14d  5888  dom2lem  6188  lt2addnq  6388  ltexnqq  6391  genpdf  6491  addnqprl  6512  addnqpru  6513  addlocpr  6519  recexprlemopl  6597  add4  6969  cnegex  6986  ltleadd  7236  zextle  8107  peano5uzti  8122  fnn0ind  8130  xrlttr  8486  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  fzaddel  8692  fzrev  8716  expivallem  8910  expival  8911  mulexp  8948  expadd  8951  expmul  8954  leexp1a  8963  bj-findis  9439
  Copyright terms: Public domain W3C validator