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

Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3r 79	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com23 78	1 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

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  1196  3imp21  1198  funopg  5252  f1o2ndf1  6231  brecop  6627  fiintim  6930  elpq  9650  xnn0lenn0nn0  9867  elfz0ubfz0  10127  elfz0fzfz0  10128  fz0fzelfz0  10129  fz0fzdiffz0  10132  fzo1fzo0n0  10185  elfzodifsumelfzo  10203  ssfzo12  10226  ssfzo12bi  10227  facwordi  10722  fihashf1rn  10770  oddnn02np1  11887  oddge22np1  11888  evennn02n  11889  evennn2n  11890  dfgcd2  12017  sqrt2irr  12164  lmodfopnelem1  13419  zabsle1  14439  bj-inf2vnlem2  14762