Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  impancom 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  2039  euotd  3991  onsucelsucr  4234  isotr  5456  ltbtwnnqq  6513  genpcdl  6617  genpcuu  6618  un0addcl  8215  un0mulcl  8216  btwnnz  8334  uznfz  8965  elfz0ubfz0  8982  fzoss1  9027  elfzo0z  9040  fzofzim  9044  elfzom1p1elfzo  9070  ssfzo12bi  9081  subfzo0  9097  expaddzap  9299  caucvgre  9580  caubnd2  9713
 Copyright terms: Public domain W3C validator