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  6593  genpcdl  6617  genpcuu  6618  recexap  7634  zaddcllemneg  8284  zdiv  8328  uzaddcl  8529  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzmlbp  8990  difelfzle  8992  fzo1fzo0n0  9039  ssfzo12bi  9081  expivallem  9256  expcllem  9266  expap0  9285  mulexp  9294  cjexp  9493  absexp  9675
 Copyright terms: Public domain W3C validator