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

Theorem impancom 260
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 115 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 124 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  eqrdav  2186  disjiun  4010  euotd  4266  onsucelsucr  4519  isotr  5830  spc2ed  6247  ltbtwnnqq  7427  genpcdl  7531  genpcuu  7532  un0addcl  9222  un0mulcl  9223  btwnnz  9360  uznfz  10116  elfz0ubfz0  10138  fzoss1  10184  elfzo0z  10197  fzofzim  10201  elfzom1p1elfzo  10227  ssfzo12bi  10238  subfzo0  10255  modfzo0difsn  10408  expaddzap  10577  caucvgre  11003  caubnd2  11139  summodc  11404  fzo0dvdseq  11876  nno  11924  lcmdvds  12092  hashgcdeq  12252  modprm0  12267  pcqcl  12319  issubg4m  13082  01eq0ring  13393  neii1  13887  neii2  13889  fsumcncntop  14296
  Copyright terms: Public domain W3C validator