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  557  an31s  560  3imp31  1185  3imp21  1187  funopg  5219  f1o2ndf1  6190  brecop  6585  fiintim  6888  elpq  9580  xnn0lenn0nn0  9795  elfz0ubfz0  10054  elfz0fzfz0  10055  fz0fzelfz0  10056  fz0fzdiffz0  10059  fzo1fzo0n0  10112  elfzodifsumelfzo  10130  ssfzo12  10153  ssfzo12bi  10154  facwordi  10647  fihashf1rn  10696  oddnn02np1  11811  oddge22np1  11812  evennn02n  11813  evennn2n  11814  dfgcd2  11941  sqrt2irr  12088  bj-inf2vnlem2  13746
  Copyright terms: Public domain W3C validator