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

Theorem mpd3an3 1244
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 1115 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpdan 406 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896
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  df-3an 898
This theorem is referenced by:  stoic2b  1335  elovmpt2  5728  oav  6064  omv  6065  oeiv  6066  f1oeng  6267  mulpipq2  6526  ltrnqg  6575  genipv  6664  subval  7265  fzrevral3  9070  fzoval  9106  subsq2  9519  bcval  9610  dvdsmul1  10121  dvdsmul2  10122
  Copyright terms: Public domain W3C validator