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

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

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2 𝜑
2 mp3an1.2 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expb 1204 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
41, 3mpan 424 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  mp3an12  1327  mp3an1i  1330  mp3anl1  1331  mp3an  1337  mp3an2i  1342  mp3an3an  1343  tfrlem9  6313  rdgexgg  6372  oaexg  6442  omexg  6445  oeiexg  6447  oav2  6457  nnaordex  6522  mulidnq  7366  1idpru  7568  addgt0sr  7752  muladd11  8067  cnegex  8112  negsubdi  8190  renegcl  8195  mulneg1  8329  ltaddpos  8386  addge01  8406  rimul  8519  recclap  8612  recidap  8619  recidap2  8620  recdivap2  8658  divdiv23apzi  8698  ltmul12a  8793  lemul12a  8795  mulgt1  8796  ltmulgt11  8797  gt0div  8803  ge0div  8804  ltdiv23i  8859  8th4div3  9114  gtndiv  9324  nn0ind  9343  fnn0ind  9345  xrre2  9795  ioorebasg  9949  fzen  10016  elfz0ubfz0  10098  expubnd  10550  le2sq2  10568  bernneq  10613  expnbnd  10616  faclbnd6  10695  bccl  10718  hashfacen  10787  shftfval  10801  mulreap  10844  caucvgrelemrec  10959  binom1p  11464  efi4p  11696  sinadd  11715  cosadd  11716  cos2t  11729  cos2tsin  11730  absefib  11749  efieq1re  11750  demoivreALT  11752  odd2np1  11848  opoe  11870  omoe  11871  opeo  11872  omeo  11873  gcdadd  11956  gcdmultiple  11991  algcvgblem  12019  algcvga  12021  isprm3  12088  coprm  12114  1arith2  12336  bl2ioo  13675  ioo2blex  13677  sinperlem  13862  logge0  13934  lgsdir2  14067  1lgs  14077
  Copyright terms: Public domain W3C validator