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

Theorem 3coml 1111
 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 1110 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1109 1 ((𝜓𝜒𝜑) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  3comr  1112  nndir  6069  f1oen2g  6235  f1dom2g  6236  ordiso  6358  addassnqg  6480  ltbtwnnqq  6513  nnanq0  6556  ltasrg  6855  recexgt0sr  6858  axmulass  6947  adddir  7018  axltadd  7089  ltleletr  7100  letr  7101  pnpcan2  7251  subdir  7383  div13ap  7672  zdiv  8328  xrletr  8724  fzen  8907  fzrevral2  8968  fzshftral  8970  fzind2  9095  elicc4abs  9690
 Copyright terms: Public domain W3C validator