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  2116  disjiun  3894  euotd  4146  onsucelsucr  4394  isotr  5685  spc2ed  6098  ltbtwnnqq  7191  genpcdl  7295  genpcuu  7296  un0addcl  8978  un0mulcl  8979  btwnnz  9113  uznfz  9851  elfz0ubfz0  9870  fzoss1  9916  elfzo0z  9929  fzofzim  9933  elfzom1p1elfzo  9959  ssfzo12bi  9970  subfzo0  9987  modfzo0difsn  10136  expaddzap  10305  caucvgre  10721  caubnd2  10857  summodc  11120  fzo0dvdseq  11482  nno  11530  lcmdvds  11687  hashgcdeq  11831  neii1  12243  neii2  12245  fsumcncntop  12652
  Copyright terms: Public domain W3C validator