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

Theorem mp3an 1243
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 1230 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 410 1 𝜃
Colors of variables: wff set class
Syntax hints:  wi 4  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:  vtocl3  2627  raltp  3455  rextp  3456  ordtriexmidlem  4273  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  ordsoexmid  4314  funopg  4962  ftp  5376  caovass  5689  caovdi  5708  ofmres  5791  mpt2fvexi  5860  dmtpos  5902  rntpos  5903  dftpos3  5908  tpostpos  5910  xpcomen  6332  1lt2pi  6496  1lt2nq  6562  halfnqq  6566  m1p1sr  6903  m1m1sr  6904  addassi  7093  mulassi  7094  adddii  7095  adddiri  7096  lttri  7181  lelttri  7182  ltletri  7183  letri  7184  mul12i  7220  mul32i  7221  add12i  7237  add32i  7238  addcani  7256  addcan2i  7257  subaddi  7361  subadd2i  7362  subsub23i  7364  addsubassi  7365  addsubi  7366  subcani  7367  subcan2i  7368  pnncani  7369  subdii  7476  subdiri  7477  ltadd2i  7489  ltadd1i  7568  leadd1i  7569  leadd2i  7570  ltsubaddi  7571  lesubaddi  7572  ltsubadd2i  7573  lesubadd2i  7574  ltaddsubi  7575  gtapii  7697  mulcanapi  7722  divclapi  7805  divcanap2i  7806  divcanap1i  7807  divrecapi  7808  divcanap3i  7809  divcanap4i  7810  divassapi  7819  divdirapi  7820  div23api  7821  div11api  7822  1mhlfehlf  8200  halfpm6th  8202  3halfnz  8395  unirnioo  8943  nnenom  9374  m1expcl2  9442  i4  9521  expnass  9524  bcn1  9626  abs3difi  9983  3dvdsdec  10176  3dvds2dec  10177  ndvdsi  10245  flodddiv4  10246  ex-fl  10279
  Copyright terms: Public domain W3C validator