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

Theorem mp3an 1232
Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
mp3an.1 𝜑
mp3an.2 𝜓
mp3an.3 𝜒
mp3an.4 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an 𝜃

Proof of Theorem mp3an
StepHypRef Expression
1 mp3an.2 . 2 𝜓
2 mp3an.3 . 2 𝜒
3 mp3an.1 . . 3 𝜑
4 mp3an.4 . . 3 ((𝜑𝜓𝜒) → 𝜃)
53, 4mp3an1 1219 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 402 1 𝜃
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  vtocl3  2610  raltp  3427  rextp  3428  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordsoexmid  4286  funopg  4934  ftp  5348  caovass  5661  caovdi  5680  ofmres  5763  mpt2fvexi  5832  dmtpos  5871  rntpos  5872  dftpos3  5877  tpostpos  5879  xpcomen  6301  1lt2pi  6436  1lt2nq  6502  halfnqq  6506  m1p1sr  6843  m1m1sr  6844  addassi  7033  mulassi  7034  adddii  7035  adddiri  7036  lttri  7120  lelttri  7121  ltletri  7122  letri  7123  mul12i  7157  mul32i  7158  add12i  7172  add32i  7173  addcani  7191  addcan2i  7192  subaddi  7296  subadd2i  7297  subsub23i  7299  addsubassi  7300  addsubi  7301  subcani  7302  subcan2i  7303  pnncani  7304  subdii  7402  subdiri  7403  ltadd2i  7415  ltadd1i  7492  leadd1i  7493  leadd2i  7494  ltsubaddi  7495  lesubaddi  7496  ltsubadd2i  7497  lesubadd2i  7498  ltaddsubi  7499  gtapii  7621  mulcanapi  7646  divclapi  7728  divcanap2i  7729  divcanap1i  7730  divrecapi  7731  divcanap3i  7732  divcanap4i  7733  divassapi  7742  divdirapi  7743  div23api  7744  div11api  7745  1mhlfehlf  8141  halfpm6th  8143  unirnioo  8840  nnenom  9184  m1expcl2  9251  i4  9329  expnass  9331  abs3difi  9726  ex-fl  9868
  Copyright terms: Public domain W3C validator