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

Theorem mp3an1 1302
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 1182 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
41, 3mpan 420 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962
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 964
This theorem is referenced by:  mp3an12  1305  mp3an1i  1308  mp3anl1  1309  mp3an  1315  mp3an2i  1320  mp3an3an  1321  tfrlem9  6216  rdgexgg  6275  oaexg  6344  omexg  6347  oeiexg  6349  oav2  6359  nnaordex  6423  mulidnq  7211  1idpru  7413  addgt0sr  7597  muladd11  7909  cnegex  7954  negsubdi  8032  renegcl  8037  mulneg1  8171  ltaddpos  8228  addge01  8248  rimul  8361  recclap  8453  recidap  8460  recidap2  8461  recdivap2  8499  divdiv23apzi  8539  ltmul12a  8632  lemul12a  8634  mulgt1  8635  ltmulgt11  8636  gt0div  8642  ge0div  8643  ltdiv23i  8698  8th4div3  8953  gtndiv  9160  nn0ind  9179  fnn0ind  9181  xrre2  9618  ioorebasg  9772  fzen  9837  elfz0ubfz0  9916  expubnd  10364  le2sq2  10382  bernneq  10426  expnbnd  10429  faclbnd6  10504  bccl  10527  hashfacen  10593  shftfval  10607  mulreap  10650  caucvgrelemrec  10765  binom1p  11268  efi4p  11437  sinadd  11456  cosadd  11457  cos2t  11470  cos2tsin  11471  absefib  11490  efieq1re  11491  demoivreALT  11493  odd2np1  11583  opoe  11605  omoe  11606  opeo  11607  omeo  11608  gcdadd  11686  gcdmultiple  11721  algcvgblem  11743  algcvga  11745  isprm3  11812  coprm  11835  bl2ioo  12727  ioo2blex  12729  sinperlem  12913  logge0  12982
  Copyright terms: Public domain W3C validator