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

Theorem 3coml 1188
Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3coml ((𝜓𝜒𝜑) → 𝜃)

Proof of Theorem 3coml
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213com23 1187 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1186 1 ((𝜓𝜒𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 962
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 depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  3comr  1189  nndir  6386  f1oen2g  6649  f1dom2g  6650  ordiso  6921  addassnqg  7204  ltbtwnnqq  7237  nnanq0  7280  ltasrg  7592  recexgt0sr  7595  axmulass  7695  adddir  7771  axltadd  7848  ltleletr  7860  letr  7861  pnpcan2  8016  subdir  8162  div13ap  8467  zdiv  9153  xrletr  9605  fzen  9837  fzrevral2  9900  fzshftral  9902  fzind2  10030  mulbinom2  10422  elicc4abs  10880  dvdsnegb  11523  muldvds1  11531  muldvds2  11532  dvdscmul  11533  dvdsmulc  11534  dvdsgcd  11713  mulgcdr  11719  lcmgcdeq  11777  congr  11794  mettri  12558  cnmet  12715  addcncntoplem  12736
  Copyright terms: Public domain W3C validator