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

Theorem mpand 413
 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 260 . 2 (𝜑 → ((𝜒𝜓) → 𝜃))
41, 3mpan2d 412 1 (𝜑 → (𝜒𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  mpani  414  mp2and  417  rspcimedv  2675  ovig  5650  prcdnql  6640  prcunqu  6641  p1le  7890  nnge1  8013  zltp1le  8356  gtndiv  8393  uzss  8589  addlelt  8786  xrre2  8835  xrre3  8836  zltaddlt1le  8975  modfzo0difsn  9345  leexp2r  9474  expnlbnd2  9542  facavg  9614  caubnd2  9944  mulcn2  10064  cn1lem  10065  climsqz  10086  climsqz2  10087  climcvg1nlem  10099  algcvgblem  10271  ialgcvga  10273
 Copyright terms: Public domain W3C validator