ILE Home 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  2169  disjiun  3982  euotd  4237  onsucelsucr  4490  isotr  5792  spc2ed  6209  ltbtwnnqq  7364  genpcdl  7468  genpcuu  7469  un0addcl  9155  un0mulcl  9156  btwnnz  9293  uznfz  10046  elfz0ubfz0  10068  fzoss1  10114  elfzo0z  10127  fzofzim  10131  elfzom1p1elfzo  10157  ssfzo12bi  10168  subfzo0  10185  modfzo0difsn  10338  expaddzap  10507  caucvgre  10932  caubnd2  11068  summodc  11333  fzo0dvdseq  11804  nno  11852  lcmdvds  12020  hashgcdeq  12180  modprm0  12195  pcqcl  12247  neii1  12900  neii2  12902  fsumcncntop  13309
  Copyright terms: Public domain W3C validator