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

Theorem exp31 346
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 108 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 108 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  exp41  352  exp42  353  expl  360  exbiri  364  anasss  379  an31s  504  con4biddc  754  3impa  1099  exp516  1124  r19.29af2  2452  mpteqb  5261  dffo3  5314  fconstfvm  5379  fliftfun  5436  tfrlem1  5923  tfrlem9  5935  nnsucsssuc  6071  nnaordex  6100  diffifi  6351  prarloclemup  6591  genpcdl  6615  genpcuu  6616  recexap  7632  zaddcllemneg  8282  zdiv  8326  uzaddcl  8527  fz0fzelfz0  8982  fz0fzdiffz0  8985  elfzmlbp  8988  difelfzle  8990  fzo1fzo0n0  9037  ssfzo12bi  9079  expivallem  9230  expcllem  9240  expap0  9259  mulexp  9268  cjexp  9467  absexp  9649
  Copyright terms: Public domain W3C validator