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

Theorem mp3an 1231
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 1218 . 2 ((ψ χ) → θ)
61, 2, 5mp2an 402 1 θ
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
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 886
This theorem is referenced by:  vtocl3  2604  raltp  3418  rextp  3419  ordtriexmidlem  4208  onsucelsucexmidlem  4214  ordsoexmid  4240  funopg  4877  ftp  5291  caovass  5603  caovdi  5622  ofmres  5705  mpt2fvexi  5774  dmtpos  5812  rntpos  5813  dftpos3  5818  tpostpos  5820  xpcomen  6237  1lt2pi  6324  1lt2nq  6389  halfnqq  6393  m1p1sr  6688  m1m1sr  6689  addassi  6833  mulassi  6834  adddii  6835  adddiri  6836  lttri  6919  lelttri  6920  ltletri  6921  letri  6922  mul12i  6956  mul32i  6957  add12i  6971  add32i  6972  addcani  6990  addcan2i  6991  subaddi  7094  subadd2i  7095  subsub23i  7097  addsubassi  7098  addsubi  7099  subcani  7100  subcan2i  7101  pnncani  7102  subdii  7200  subdiri  7201  ltadd2i  7213  ltadd1i  7289  leadd1i  7290  leadd2i  7291  ltsubaddi  7292  lesubaddi  7293  ltsubadd2i  7294  lesubadd2i  7295  ltaddsubi  7296  mulcanapi  7430  divclapi  7512  divcanap2i  7513  divcanap1i  7514  divrecapi  7515  divcanap3i  7516  divcanap4i  7517  divassapi  7526  divdirapi  7527  div23api  7528  div11api  7529  1mhlfehlf  7920  halfpm6th  7922  unirnioo  8612  nnenom  8891  m1expcl2  8931  i4  9008  expnass  9010
  Copyright terms: Public domain W3C validator