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

Theorem mp3an12 1222
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mp3an12.1 𝜑
mp3an12.2 𝜓
mp3an12.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an12 (𝜒𝜃)

Proof of Theorem mp3an12
StepHypRef Expression
1 mp3an12.2 . 2 𝜓
2 mp3an12.1 . . 3 𝜑
3 mp3an12.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
42, 3mp3an1 1219 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 400 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:  ceqsralv  2585  brelrn  4567  funpr  4951  ener  6259  ltaddnq  6503  ltadd1sr  6859  mul02  7382  ltapi  7623  div0ap  7677  divclapzi  7721  divcanap1zi  7722  divcanap2zi  7723  divrecapzi  7724  divcanap3zi  7725  divcanap4zi  7726  divassapzi  7736  divmulapzi  7737  divdirapzi  7738  redivclapzi  7752  ltm1  7810  mulgt1  7827  recgt1i  7862  recreclt  7864  ltmul1i  7884  ltdiv1i  7885  ltmuldivi  7886  ltmul2i  7887  lemul1i  7888  lemul2i  7889  cju  7911  nnge1  7935  nngt0  7937  nnrecgt0  7949  elnnnn0c  8225  elnnz1  8266  recnz  8331  eluzsubi  8498  ge0gtmnf  8734  m1expcl2  9251  1exp  9258  expubnd  9285  expnbnd  9346  expnlbnd  9347  remim  9434  imval2  9468  cjdivapi  9509  absdivapzi  9724
  Copyright terms: Public domain W3C validator