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

Theorem 3coml 1212
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 1211 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1210 1 ((𝜓𝜒𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  3comr  1213  nndir  6515  f1oen2g  6781  f1dom2g  6782  ordiso  7065  addassnqg  7411  ltbtwnnqq  7444  nnanq0  7487  ltasrg  7799  recexgt0sr  7802  axmulass  7902  adddir  7978  axltadd  8057  ltleletr  8069  letr  8070  pnpcan2  8227  subdir  8373  div13ap  8680  zdiv  9371  xrletr  9838  fzen  10073  fzrevral2  10136  fzshftral  10138  fzind2  10269  mulbinom2  10668  elicc4abs  11135  dvdsnegb  11847  muldvds1  11855  muldvds2  11856  dvdscmul  11857  dvdsmulc  11858  dvdsgcd  12045  mulgcdr  12051  lcmgcdeq  12115  congr  12132  mulgnnass  13097  mettri  14333  cnmet  14490  addcncntoplem  14511
  Copyright terms: Public domain W3C validator