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

Theorem com13 78
Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com13 (𝜒 → (𝜓 → (𝜑𝜃)))

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3r 77 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 76 1 (𝜒 → (𝜓 → (𝜑𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  com24  85  an13s  509  an31s  512  funopg  4962  f1o2ndf1  5877  brecop  6227  elfz0ubfz0  9084  elfz0fzfz0  9085  fz0fzelfz0  9086  fz0fzdiffz0  9089  fzo1fzo0n0  9141  elfzodifsumelfzo  9159  ssfzo12  9182  ssfzo12bi  9183  facwordi  9608  oddnn02np1  10192  oddge22np1  10193  evennn02n  10194  evennn2n  10195  sqrt2irr  10251  bj-inf2vnlem2  10483
  Copyright terms: Public domain W3C validator