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

Theorem 3imp 1097
 Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1 (φ → (ψ → (χθ)))
Assertion
Ref Expression
3imp ((φ ψ χ) → θ)

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 886 . 2 ((φ ψ χ) ↔ ((φ ψ) χ))
2 3imp.1 . . 3 (φ → (ψ → (χθ)))
32imp31 243 . 2 (((φ ψ) χ) → θ)
41, 3sylbi 114 1 ((φ ψ χ) → θ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100 This theorem depends on definitions:  df-bi 110  df-3an 886 This theorem is referenced by:  3impa  1098  3impb  1099  3impia  1100  3impib  1101  3com23  1109  3an1rs  1115  3imp1  1116  3impd  1117  syl3an2  1168  syl3an3  1169  3jao  1195  biimp3ar  1235  poxp  5794  tfrlemibxssdm  5882  nndi  6004  nnmass  6005  difelfzle  8762  fzo1fzo0n0  8809  elfzo0z  8810  fzofzim  8814  elfzodifsumelfzo  8827  mulexp  8948  expadd  8951  expmul  8954  bernneq  9022
 Copyright terms: Public domain W3C validator