ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantll Structured version   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  6490  addnqprl  6511  addnqpru  6512  addlocpr  6518  recexprlemopl  6596  add4  6949  cnegex  6966  ltleadd  7216  zextle  8087  peano5uzti  8102  fnn0ind  8110  xrlttr  8466  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  fzaddel  8672  fzrev  8696  expivallem  8890  expival  8891  mulexp  8928  expadd  8931  expmul  8934  leexp1a  8943  bj-findis  9409
  Copyright terms: Public domain W3C validator