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

Theorem impancom 258
 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 114 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 123 1 ((𝜑𝜒) → (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem is referenced by:  eqrdav  2139  disjiun  3931  euotd  4183  onsucelsucr  4431  isotr  5724  spc2ed  6137  ltbtwnnqq  7246  genpcdl  7350  genpcuu  7351  un0addcl  9033  un0mulcl  9034  btwnnz  9168  uznfz  9913  elfz0ubfz0  9932  fzoss1  9978  elfzo0z  9991  fzofzim  9995  elfzom1p1elfzo  10021  ssfzo12bi  10032  subfzo0  10049  modfzo0difsn  10198  expaddzap  10367  caucvgre  10784  caubnd2  10920  summodc  11183  fzo0dvdseq  11589  nno  11637  lcmdvds  11794  hashgcdeq  11938  neii1  12353  neii2  12355  fsumcncntop  12762
 Copyright terms: Public domain W3C validator