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

Theorem 3coml 1156
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 1155 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1154 1 ((𝜓𝜒𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 932
This theorem is referenced by:  3comr  1157  nndir  6316  f1oen2g  6579  f1dom2g  6580  ordiso  6836  addassnqg  7091  ltbtwnnqq  7124  nnanq0  7167  ltasrg  7466  recexgt0sr  7469  axmulass  7558  adddir  7629  axltadd  7706  ltleletr  7717  letr  7718  pnpcan2  7873  subdir  8015  div13ap  8314  zdiv  8991  xrletr  9432  fzen  9664  fzrevral2  9727  fzshftral  9729  fzind2  9857  mulbinom2  10249  elicc4abs  10706  dvdsnegb  11305  muldvds1  11313  muldvds2  11314  dvdscmul  11315  dvdsmulc  11316  dvdsgcd  11493  mulgcdr  11499  lcmgcdeq  11557  congr  11574  mettri  12301  cnmet  12452
  Copyright terms: Public domain W3C validator