ILE Home 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  567  an31s  570  3imp31  1198  3imp21  1200  funopg  5289  f1o2ndf1  6283  brecop  6681  fiintim  6987  elpq  9717  xnn0lenn0nn0  9934  elfz0ubfz0  10194  elfz0fzfz0  10195  fz0fzelfz0  10196  fz0fzdiffz0  10199  fzo1fzo0n0  10253  elfzodifsumelfzo  10271  ssfzo12  10294  ssfzo12bi  10295  facwordi  10814  fihashf1rn  10862  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  dfgcd2  12154  sqrt2irr  12303  lmodfopnelem1  13823  mpomulcn  14745  zabsle1  15156  gausslemma2dlem1a  15215  2lgsoddprm  15270  bj-inf2vnlem2  15533
  Copyright terms: Public domain W3C validator