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

Theorem 3coml 1146
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 1145 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1144 1 ((𝜓𝜒𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3comr  1147  nndir  6182  f1oen2g  6401  f1dom2g  6402  ordiso  6635  addassnqg  6843  ltbtwnnqq  6876  nnanq0  6919  ltasrg  7218  recexgt0sr  7221  axmulass  7310  adddir  7381  axltadd  7458  ltleletr  7469  letr  7470  pnpcan2  7624  subdir  7766  div13ap  8057  zdiv  8729  xrletr  9167  fzen  9351  fzrevral2  9412  fzshftral  9414  fzind2  9538  mulbinom2  9904  elicc4abs  10353  dvdsnegb  10592  muldvds1  10600  muldvds2  10601  dvdscmul  10602  dvdsmulc  10603  dvdsgcd  10780  mulgcdr  10786  lcmgcdeq  10844  congr  10861
  Copyright terms: Public domain W3C validator