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  2658  ovig  5622  prcdnql  6582  prcunqu  6583  p1le  7815  nnge1  7937  zltp1le  8298  gtndiv  8335  uzss  8493  xrre2  8734  xrre3  8735  leexp2r  9308  expnlbnd2  9374  caubnd2  9713  mulcn2  9833  cn1lem  9834  climsqz  9855  climsqz2  9856  climcvg1nlem  9868  algcvgblem  9888  ialgcvga  9890
 Copyright terms: Public domain W3C validator