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  477  ad2ant2rl  480  3ad2antr2  1069  3ad2antr3  1070  xordidc  1287  foco  5059  fvun1  5182  isocnv  5394  isores2  5396  f1oiso2  5409  offval  5661  xp2nd  5735  1stconst  5784  2ndconst  5785  tfrlem9  5876  nnmordi  6025  dom2lem  6188  fundmen  6222  ltsonq  6382  ltexnqq  6391  genprndl  6504  genprndu  6505  ltpopr  6567  ltsopr  6568  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemdisj  6578  ltexprlemfl  6581  ltexprlemfu  6583  mulcmpblnrlemg  6628  cnegexlem2  6944  muladd  7137  divadddivap  7445  ltmul12a  7567  lemul12b  7568  cju  7654  zextlt  8068  xrre  8463  ixxdisj  8502  iooshf  8551  icodisj  8590  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  iccf1o  8602  fzaddel  8652  fzsubel  8653  expineg2  8878  expsubap  8916  expnbnd  8985
  Copyright terms: Public domain W3C validator