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

Theorem adantll 448
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  462  ad2ant2l  465  ad2ant2lr  467  3ad2antl3  1056  3adant1l  1113  reu6  2707  sbc2iegf  2805  sbcralt  2811  sbcrext  2812  indifdir  3170  pofun  4023  poinxp  4336  ssimaex  5159  fndmdif  5197  dffo4  5240  foco2  5243  fcompt  5258  fconst2g  5301  foeqcnvco  5355  f1eqcocnv  5356  fliftel1  5359  isores3  5380  acexmid  5435  tfrlemi14d  5868  lt2addnq  6263  ltexnqq  6266  genpdf  6362  addnqprl  6384  addnqpru  6385  addlocpr  6391  recexprlemopl  6459  add4  6765  cnegex  6782  ltleadd  7032  bj-findis  7344
  Copyright terms: Public domain W3C validator