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

Theorem exp31 356
 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 113 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 113 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106 This theorem is referenced by:  exp41  362  exp42  363  expl  370  exbiri  374  anasss  391  an31s  535  con4biddc  788  3impa  1134  exp516  1159  r19.29af2  2502  mpteqb  5315  dffo3  5368  fconstfvm  5433  fliftfun  5489  tfrlem1  5979  tfrlem9  5990  tfr1onlemaccex  6019  tfrcllemaccex  6032  tfrcl  6035  nnsucsssuc  6158  nnaordex  6189  diffifi  6452  prarloclemup  6824  genpcdl  6848  genpcuu  6849  negf1o  7630  recexap  7887  zaddcllemneg  8548  zdiv  8593  uzaddcl  8832  fz0fzelfz0  9292  fz0fzdiffz0  9295  elfzmlbp  9297  difelfzle  9299  fzo1fzo0n0  9346  ssfzo12bi  9388  exfzdc  9403  modfzo0difsn  9554  frecuzrdgg  9575  iseqvalt  9609  expivallem  9651  expcllem  9661  expap0  9680  mulexp  9689  cjexp  10006  absexp  10191  fimaxre2  10335  divconjdvds  10482  addmodlteqALT  10492  divalglemeunn  10553  divalglemeuneg  10555  zsupcllemstep  10573  bezoutlemstep  10618  bezoutlemmain  10619  dfgcd2  10635  pw2dvdslemn  10775
 Copyright terms: Public domain W3C validator