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

Theorem mpand 405
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpand.1 (φψ)
mpand.2 (φ → ((ψ χ) → θ))
Assertion
Ref Expression
mpand (φ → (χθ))

Proof of Theorem mpand
StepHypRef Expression
1 mpand.1 . 2 (φψ)
2 mpand.2 . . 3 (φ → ((ψ χ) → θ))
32ancomsd 256 . 2 (φ → ((χ ψ) → θ))
41, 3mpan2d 404 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:  mpani  406  mp2and  409  rspcimedv  2652  ovig  5564  prcdnql  6467  prcunqu  6468  p1le  7596  nnge1  7718  zltp1le  8074  gtndiv  8111  uzss  8269  xrre2  8504  xrre3  8505  leexp2r  8962  expnlbnd2  9027
  Copyright terms: Public domain W3C validator