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

Theorem mp3an2 1320
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an2.1 𝜓
mp3an2.2 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an2 ((𝜑𝜒) → 𝜃)

Proof of Theorem mp3an2
StepHypRef Expression
1 mp3an2.1 . 2 𝜓
2 mp3an2.2 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expa 1198 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 433 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 973
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 975
This theorem is referenced by:  mp3anl2  1327  ordin  4368  ordsuc  4545  omv  6432  oeiv  6433  omv2  6442  1idprl  7545  muladd11  8045  negsub  8160  subneg  8161  ltaddneg  8336  muleqadd  8579  diveqap1  8615  conjmulap  8639  nnsub  8910  addltmul  9107  zltp1le  9259  gtndiv  9300  eluzp1m1  9503  xnn0le2is012  9816  divelunit  9952  fznatpl1  10025  flqbi2  10240  flqdiv  10270  frecfzen2  10376  nn0ennn  10382  faclbnd3  10670  shftfvalg  10775  ovshftex  10776  shftfval  10778  abs2dif  11063  cos2t  11706  sin01gt0  11717  cos01gt0  11718  demoivre  11728  demoivreALT  11729  omeo  11850  gcd0id  11927  sqgcd  11977  isprm3  12065  eulerthlemth  12179  pczpre  12244  pcrec  12255  setscom  12449  setsslid  12459  setsslnid  12460  abssinper  13526  lgs1  13704
  Copyright terms: Public domain W3C validator