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

Theorem mpd3an3 1316
 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 1181 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpdan 417 1 ((𝜑𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962 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  df-3an 964 This theorem is referenced by:  stoic2b  1406  elovmpo  5964  oav  6343  omv  6344  oeiv  6345  f1oeng  6644  mulpipq2  7172  ltrnqg  7221  genipv  7310  subval  7947  subap0  8398  xaddval  9621  fzrevral3  9880  fzoval  9918  subsq2  10393  bcval  10488  dvdsmul1  11504  dvdsmul2  11505  gcdval  11637  eucalgval2  11723  setsvalg  11978  restval  12115  restin  12334  hmeofvalg  12461  cncfval  12717
 Copyright terms: Public domain W3C validator