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

Theorem 3coml 1173
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 1172 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1171 1 ((𝜓𝜒𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
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 949
This theorem is referenced by:  3comr  1174  nndir  6354  f1oen2g  6617  f1dom2g  6618  ordiso  6889  addassnqg  7158  ltbtwnnqq  7191  nnanq0  7234  ltasrg  7546  recexgt0sr  7549  axmulass  7649  adddir  7725  axltadd  7802  ltleletr  7814  letr  7815  pnpcan2  7970  subdir  8116  div13ap  8421  zdiv  9107  xrletr  9559  fzen  9791  fzrevral2  9854  fzshftral  9856  fzind2  9984  mulbinom2  10376  elicc4abs  10834  dvdsnegb  11437  muldvds1  11445  muldvds2  11446  dvdscmul  11447  dvdsmulc  11448  dvdsgcd  11627  mulgcdr  11633  lcmgcdeq  11691  congr  11708  mettri  12469  cnmet  12626  addcncntoplem  12647
  Copyright terms: Public domain W3C validator