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

Theorem exp31 350
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 112 . 2 ((𝜑𝜓) → (𝜒𝜃))
32ex 112 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  exp41  356  exp42  357  expl  364  exbiri  368  anasss  385  an31s  512  con4biddc  765  3impa  1110  exp516  1135  r19.29af2  2469  mpteqb  5288  dffo3  5341  fconstfvm  5406  fliftfun  5463  tfrlem1  5953  tfrlem9  5965  nnsucsssuc  6101  nnaordex  6130  diffifi  6381  prarloclemup  6650  genpcdl  6674  genpcuu  6675  recexap  7707  zaddcllemneg  8340  zdiv  8385  uzaddcl  8624  fz0fzelfz0  9085  fz0fzdiffz0  9088  elfzmlbp  9091  difelfzle  9093  fzo1fzo0n0  9140  ssfzo12bi  9182  modfzo0difsn  9344  expivallem  9420  expcllem  9430  expap0  9449  mulexp  9458  cjexp  9720  absexp  9905  divconjdvds  10160  addmodlteqALT  10170  pw2dvdslemn  10232
  Copyright terms: Public domain W3C validator