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

Theorem 3coml 1122
 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 1121 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1120 1 ((𝜓𝜒𝜑) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 896 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114  df-3an 898 This theorem is referenced by:  3comr  1123  nndir  6099  f1oen2g  6265  f1dom2g  6266  ordiso  6415  addassnqg  6537  ltbtwnnqq  6570  nnanq0  6613  ltasrg  6912  recexgt0sr  6915  axmulass  7004  adddir  7075  axltadd  7147  ltleletr  7158  letr  7159  pnpcan2  7313  subdir  7454  div13ap  7745  zdiv  8385  xrletr  8824  fzen  9008  fzrevral2  9069  fzshftral  9071  fzind2  9196  mulbinom2  9532  elicc4abs  9920  dvdsnegb  10124  muldvds1  10131  muldvds2  10132  dvdscmul  10133  dvdsmulc  10134
 Copyright terms: Public domain W3C validator