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  858  3impa  1196  exp516  1229  rexlimdva2  2614  r19.29af2  2634  disjiun  4025  mpteqb  5649  dffo3  5706  fconstfvm  5777  fliftfun  5840  tfrlem1  6363  tfrlem9  6374  tfr1onlemaccex  6403  tfrcllemaccex  6416  tfrcl  6419  nnsucsssuc  6547  nnaordex  6583  diffifi  6952  fidcenumlemrk  7015  fidcenumlemr  7016  nninfninc  7184  nnnninfeq  7189  nnnninfeq2  7190  exmidontriimlem4  7286  exmidontriim  7287  prarloclemup  7557  genpcdl  7581  genpcuu  7582  negf1o  8403  recexap  8674  zaddcllemneg  9359  zdiv  9408  uzaddcl  9654  fz0fzelfz0  10196  fz0fzdiffz0  10199  elfzmlbp  10201  difelfzle  10203  fzo1fzo0n0  10253  ssfzo12bi  10295  exfzdc  10310  modfzo0difsn  10469  frecuzrdgg  10490  seq3val  10534  seqvalcd  10535  seqf1og  10595  exp3vallem  10614  expcllem  10624  expap0  10643  mulexp  10652  cjexp  11040  absexp  11226  fimaxre2  11373  summodc  11529  fsum2d  11581  modfsummod  11604  binom  11630  clim2prod  11685  fprod2d  11769  efexp  11828  demoivreALT  11920  divconjdvds  11994  addmodlteqALT  12004  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemstep  12085  bezoutlemstep  12137  bezoutlemmain  12138  dfgcd2  12154  pw2dvdslemn  12306  oddprmdvds  12495  sgrpidmndm  13004  gsumfzz  13070  srgmulgass  13488  ringinvnzdiv  13549  lmodvsmmulgdi  13822  topbas  14246  cnplimclemr  14848  limccnp2lem  14855  gausslemma2dlem3  15220  nninfalllem1  15568  nninfsellemdc  15570  nninfsellemqall  15575  isomninnlem  15590  trirec0  15604  ismkvnnlem  15612
  Copyright terms: Public domain W3C validator