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

Theorem com13 80
 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 79 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 78 1 (𝜒 → (𝜓 → (𝜑𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  com24  87  an13s  556  an31s  559  funopg  5157  f1o2ndf1  6125  brecop  6519  fiintim  6817  xnn0lenn0nn0  9655  elfz0ubfz0  9909  elfz0fzfz0  9910  fz0fzelfz0  9911  fz0fzdiffz0  9914  fzo1fzo0n0  9967  elfzodifsumelfzo  9985  ssfzo12  10008  ssfzo12bi  10009  facwordi  10493  fihashf1rn  10542  oddnn02np1  11584  oddge22np1  11585  evennn02n  11586  evennn2n  11587  dfgcd2  11709  sqrt2irr  11847  bj-inf2vnlem2  13183
 Copyright terms: Public domain W3C validator