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

Theorem exp31 364
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp31.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
exp31 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem exp31
StepHypRef Expression
1 exp31.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21ex 115 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 115 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  exp41  370  exp42  371  expl  378  exbiri  382  anasss  399  an31s  570  con4biddc  857  3impa  1194  exp516  1227  rexlimdva2  2597  r19.29af2  2617  disjiun  3995  mpteqb  5601  dffo3  5658  fconstfvm  5729  fliftfun  5790  tfrlem1  6302  tfrlem9  6313  tfr1onlemaccex  6342  tfrcllemaccex  6355  tfrcl  6358  nnsucsssuc  6486  nnaordex  6522  diffifi  6887  fidcenumlemrk  6946  fidcenumlemr  6947  nnnninfeq  7119  nnnninfeq2  7120  exmidontriimlem4  7216  exmidontriim  7217  prarloclemup  7472  genpcdl  7496  genpcuu  7497  negf1o  8316  recexap  8586  zaddcllemneg  9268  zdiv  9317  uzaddcl  9562  fz0fzelfz0  10100  fz0fzdiffz0  10103  elfzmlbp  10105  difelfzle  10107  fzo1fzo0n0  10156  ssfzo12bi  10198  exfzdc  10213  modfzo0difsn  10368  frecuzrdgg  10389  seq3val  10431  seqvalcd  10432  exp3vallem  10494  expcllem  10504  expap0  10523  mulexp  10532  cjexp  10873  absexp  11059  fimaxre2  11206  summodc  11362  fsum2d  11414  modfsummod  11437  binom  11463  clim2prod  11518  fprod2d  11602  efexp  11661  demoivreALT  11752  divconjdvds  11825  addmodlteqALT  11835  divalglemeunn  11896  divalglemeuneg  11898  zsupcllemstep  11916  bezoutlemstep  11968  bezoutlemmain  11969  dfgcd2  11985  pw2dvdslemn  12135  oddprmdvds  12322  sgrpidmndm  12700  srgmulgass  12985  ringinvnzdiv  13040  topbas  13200  cnplimclemr  13771  limccnp2lem  13778  nninfalllem1  14380  nninfsellemdc  14382  nninfsellemqall  14387  isomninnlem  14401  trirec0  14415  ismkvnnlem  14423
  Copyright terms: Public domain W3C validator