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

Theorem mp3an2 1304
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 1182 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 432 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
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 965
This theorem is referenced by:  mp3anl2  1311  ordin  4314  ordsuc  4485  omv  6358  oeiv  6359  omv2  6368  1idprl  7421  muladd11  7918  negsub  8033  subneg  8034  ltaddneg  8209  muleqadd  8452  diveqap1  8488  conjmulap  8512  nnsub  8782  addltmul  8979  zltp1le  9131  gtndiv  9169  eluzp1m1  9372  xnn0le2is012  9678  divelunit  9814  fznatpl1  9886  flqbi2  10094  flqdiv  10124  frecfzen2  10230  nn0ennn  10236  faclbnd3  10520  shftfvalg  10621  ovshftex  10622  shftfval  10624  abs2dif  10909  cos2t  11491  sin01gt0  11502  cos01gt0  11503  demoivre  11513  demoivreALT  11514  omeo  11629  gcd0id  11701  sqgcd  11751  isprm3  11833  setscom  12036  setsslid  12046  setsslnid  12047  abssinper  12973
  Copyright terms: Public domain W3C validator