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

Theorem mp2and 409
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 405 . 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  3284  tfisi  4253  tfr0  5878  ertrd  6058  th3qlem1  6144  ltbtwnnqq  6398  prarloclemarch2  6402  addlocprlemeqgt  6515  addnqpr1lemrl  6537  addnqpr1lemru  6538  ltexprlemrl  6582  ltexprlemru  6584  addcanprleml  6586  addcanprlemu  6587  recexprlemloc  6601  recexprlem1ssu  6604  letrd  6895  lelttrd  6896  lttrd  6897  ltletrd  7176  le2addd  7309  le2subd  7310  ltleaddd  7311  leltaddd  7312  lt2subd  7314  ltmul12a  7567  lediv12a  7601  lemul12ad  7649  lemul12bd  7650  lt2halvesd  7909  uzind  8085  uztrn  8225  xrlttrd  8455  xrlelttrd  8456  xrltletrd  8457  xrletrd  8458  ixxss1  8503  ixxss2  8504  ixxss12  8505
  Copyright terms: Public domain W3C validator