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

Theorem com13 79
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 78 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 77 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  86  an13s  534  an31s  537  funopg  5048  f1o2ndf1  5993  brecop  6382  fiintim  6639  elfz0ubfz0  9536  elfz0fzfz0  9537  fz0fzelfz0  9538  fz0fzdiffz0  9541  fzo1fzo0n0  9594  elfzodifsumelfzo  9612  ssfzo12  9635  ssfzo12bi  9636  facwordi  10148  fihashf1rn  10197  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161  dfgcd2  11281  sqrt2irr  11419  bj-inf2vnlem2  11866
  Copyright terms: Public domain W3C validator