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

Theorem mp2and 411
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1 (φψ)
mp2and.2 (φχ)
mp2and.3 (φ → ((ψ χ) → θ))
Assertion
Ref Expression
mp2and (φθ)

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2 (φχ)
2 mp2and.1 . . 3 (φψ)
3 mp2and.3 . . 3 (φ → ((ψ χ) → θ))
42, 3mpand 407 . 2 (φ → (χθ))
51, 4mpd 13 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 depends on definitions:  df-bi 110
This theorem is referenced by:  ssnelpssd  3263  tfisi  4233  ertrd  6029  th3qlem1  6115  ltbtwnnqq  6266  prarloclemarch2  6270  addlocprlemeqgt  6381  ltexprlemrl  6441  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  recexprlemloc  6459  recexprlem1ssu  6462  letrd  6725  lelttrd  6726  lttrd  6727  ltletrd  7006  le2addd  7135  le2subd  7136  ltleaddd  7137  leltaddd  7138  lt2subd  7140
  Copyright terms: Public domain W3C validator