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  4370  ordsuc  4547  omv  6434  oeiv  6435  omv2  6444  1idprl  7552  muladd11  8052  negsub  8167  subneg  8168  ltaddneg  8343  muleqadd  8586  diveqap1  8622  conjmulap  8646  nnsub  8917  addltmul  9114  zltp1le  9266  gtndiv  9307  eluzp1m1  9510  xnn0le2is012  9823  divelunit  9959  fznatpl1  10032  flqbi2  10247  flqdiv  10277  frecfzen2  10383  nn0ennn  10389  faclbnd3  10677  shftfvalg  10782  ovshftex  10783  shftfval  10785  abs2dif  11070  cos2t  11713  sin01gt0  11724  cos01gt0  11725  demoivre  11735  demoivreALT  11736  omeo  11857  gcd0id  11934  sqgcd  11984  isprm3  12072  eulerthlemth  12186  pczpre  12251  pcrec  12262  setscom  12456  setsslid  12466  setsslnid  12467  abssinper  13561  lgs1  13739
  Copyright terms: Public domain W3C validator