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

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

Proof of Theorem adantrl
StepHypRef Expression
1 simpr 103 . 2 ((θ ψ) → ψ)
2 adant2.1 . 2 ((φ ψ) → χ)
31, 2sylan2 270 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:  ad2ant2l  462  ad2ant2rl  465  3ad2antr2  1052  3ad2antr3  1053  xordidc  1269  foco  5030  fvun1  5153  isocnv  5365  isores2  5367  f1oiso2  5380  offval  5631  xp2nd  5705  1stconst  5754  2ndconst  5755  tfrlem9  5846  nnmordi  5989  ltsonq  6244  ltexnqq  6253  genprndl  6363  genprndu  6364  ltpopr  6419  ltsopr  6420  ltexprlemm  6424  ltexprlemopl  6425  ltexprlemopu  6427  ltexprlemdisj  6430  ltexprlemfl  6433  ltexprlemfu  6435  mulcmpblnrlemg  6479  cnegexlem2  6788  muladd  6981  divadddivap  7289  ltmul12a  7410  lemul12b  7411  cju  7497  zextlt  7898  xrre  8210
  Copyright terms: Public domain W3C validator