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

Theorem mpand 425
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 267 . 2 (𝜑 → ((𝜒𝜓) → 𝜃))
41, 3mpan2d 424 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpani  426  mp2and  429  rspcimedv  2765  ovig  5860  prcdnql  7260  prcunqu  7261  p1le  8575  nnge1  8711  zltp1le  9076  gtndiv  9114  uzss  9314  addlelt  9523  xrre2  9572  xrre3  9573  zltaddlt1le  9757  modfzo0difsn  10136  leexp2r  10315  expnlbnd2  10385  facavg  10460  caubnd2  10857  maxleast  10953  mulcn2  11049  cn1lem  11051  climsqz  11072  climsqz2  11073  climcvg1nlem  11086  fsumabs  11202  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  zsupcllemstep  11565  gcdzeq  11637  algcvgblem  11657  algcvga  11659  lcmdvdsb  11692  coprm  11749  bldisj  12497  xblm  12513  metss2lem  12593  bdxmet  12597  limccoap  12743
  Copyright terms: Public domain W3C validator