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  2203  disjiun  4038  euotd  4298  onsucelsucr  4555  isotr  5884  spc2ed  6318  nninfninc  7224  ltbtwnnqq  7527  genpcdl  7631  genpcuu  7632  un0addcl  9327  un0mulcl  9328  btwnnz  9466  uznfz  10224  elfz0ubfz0  10246  fzoss1  10293  elfzo0z  10306  fzofzim  10310  elfzom1p1elfzo  10341  ssfzo12bi  10352  subfzo0  10369  modfzo0difsn  10538  expaddzap  10726  caucvgre  11234  caubnd2  11370  summodc  11636  fzo0dvdseq  12110  nno  12159  lcmdvds  12343  hashgcdeq  12504  modprm0  12519  pcqcl  12571  issubg4m  13471  01eq0ring  13893  neii1  14561  neii2  14563  fsumcncntop  14981  gausslemma2dlem1a  15477
  Copyright terms: Public domain W3C validator