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

Theorem impancom 251
 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 112 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 76 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 119 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-ia1 103  ax-ia2 104  ax-ia3 105 This theorem is referenced by:  eqrdav  2055  euotd  4019  onsucelsucr  4262  isotr  5484  spc2ed  5882  ltbtwnnqq  6571  genpcdl  6675  genpcuu  6676  un0addcl  8272  un0mulcl  8273  btwnnz  8392  uznfz  9067  elfz0ubfz0  9084  fzoss1  9129  elfzo0z  9142  fzofzim  9146  elfzom1p1elfzo  9172  ssfzo12bi  9183  subfzo0  9199  modfzo0difsn  9345  expaddzap  9464  caucvgre  9808  caubnd2  9944  fzo0dvdseq  10169  nno  10218
 Copyright terms: Public domain W3C validator