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

Theorem mpd3an3 1270
Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
Hypotheses
Ref Expression
mpd3an3.2 ((𝜑𝜓) → 𝜒)
mpd3an3.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mpd3an3 ((𝜑𝜓) → 𝜃)

Proof of Theorem mpd3an3
StepHypRef Expression
1 mpd3an3.2 . 2 ((𝜑𝜓) → 𝜒)
2 mpd3an3.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expa 1139 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpdan 412 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  stoic2b  1360  elovmpt2  5753  oav  6119  omv  6120  oeiv  6121  f1oeng  6326  mulpipq2  6693  ltrnqg  6742  genipv  6831  subval  7437  fzrevral3  9270  fzoval  9305  subsq2  9749  bcval  9843  dvdsmul1  10443  dvdsmul2  10444  gcdval  10576  eucalgval2  10660
  Copyright terms: Public domain W3C validator