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

Theorem impancom 247
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
Hypothesis
Ref Expression
impancom.1 ((φ ψ) → (χθ))
Assertion
Ref Expression
impancom ((φ χ) → (ψθ))

Proof of Theorem impancom
StepHypRef Expression
1 impancom.1 . . . 4 ((φ ψ) → (χθ))
21ex 108 . . 3 (φ → (ψ → (χθ)))
32com23 72 . 2 (φ → (χ → (ψθ)))
43imp 115 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-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  eqrdav  2036  euotd  3982  onsucelsucr  4199  isotr  5399  ltbtwnnqq  6398  genpcdl  6501  genpcuu  6502  un0addcl  7971  un0mulcl  7972  btwnnz  8090  uznfz  8715  elfz0ubfz0  8732  fzoss1  8777  elfzo0z  8790  fzofzim  8794  elfzom1p1elfzo  8820  ssfzo12bi  8831  expaddzap  8933
  Copyright terms: Public domain W3C validator