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

Theorem mp3an1 1270
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 1150 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
41, 3mpan 418 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  mp3an12  1273  mp3an1i  1276  mp3anl1  1277  mp3an  1283  mp3an2i  1288  mp3an3an  1289  tfrlem9  6146  rdgexgg  6205  oaexg  6274  omexg  6277  oeiexg  6279  oav2  6289  nnaordex  6353  mulidnq  7098  1idpru  7300  addgt0sr  7471  muladd11  7766  cnegex  7811  negsubdi  7889  renegcl  7894  mulneg1  8024  ltaddpos  8081  addge01  8101  rimul  8213  recclap  8300  recidap  8307  recidap2  8308  recdivap2  8346  divdiv23apzi  8386  ltmul12a  8476  lemul12a  8478  mulgt1  8479  ltmulgt11  8480  gt0div  8486  ge0div  8487  ltdiv23i  8542  8th4div3  8791  gtndiv  8998  nn0ind  9017  fnn0ind  9019  xrre2  9445  ioorebasg  9599  fzen  9664  elfz0ubfz0  9743  expubnd  10191  le2sq2  10209  bernneq  10253  expnbnd  10256  faclbnd6  10331  bccl  10354  hashfacen  10420  shftfval  10434  mulreap  10477  caucvgrelemrec  10591  binom1p  11093  efi4p  11222  sinadd  11241  cosadd  11242  cos2t  11255  cos2tsin  11256  absefib  11274  efieq1re  11275  demoivreALT  11277  odd2np1  11365  opoe  11387  omoe  11388  opeo  11389  omeo  11390  gcdadd  11468  gcdmultiple  11501  algcvgblem  11523  algcvga  11525  isprm3  11592  coprm  11615  bl2ioo  12461  ioo2blex  12463
  Copyright terms: Public domain W3C validator