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

Theorem mpand 426
 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 425 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  427  mp2and  430  rspcimedv  2796  ovig  5901  prcdnql  7336  prcunqu  7337  p1le  8651  nnge1  8787  zltp1le  9152  gtndiv  9190  uzss  9390  addlelt  9605  xrre2  9654  xrre3  9655  zltaddlt1le  9840  modfzo0difsn  10219  leexp2r  10398  expnlbnd2  10468  facavg  10544  caubnd2  10941  maxleast  11037  mulcn2  11133  cn1lem  11135  climsqz  11156  climsqz2  11157  climcvg1nlem  11170  fsumabs  11286  cvgratnnlemnexp  11345  cvgratnnlemmn  11346  zsupcllemstep  11694  gcdzeq  11766  algcvgblem  11786  algcvga  11788  lcmdvdsb  11821  coprm  11878  bldisj  12629  xblm  12645  metss2lem  12725  bdxmet  12729  limccoap  12875
 Copyright terms: Public domain W3C validator