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  1198  3imp21  1200  funopg  5288  f1o2ndf1  6281  brecop  6679  fiintim  6985  elpq  9714  xnn0lenn0nn0  9931  elfz0ubfz0  10191  elfz0fzfz0  10192  fz0fzelfz0  10193  fz0fzdiffz0  10196  fzo1fzo0n0  10250  elfzodifsumelfzo  10268  ssfzo12  10291  ssfzo12bi  10292  facwordi  10811  fihashf1rn  10859  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  dfgcd2  12151  sqrt2irr  12300  lmodfopnelem1  13820  zabsle1  15115  gausslemma2dlem1a  15174  bj-inf2vnlem2  15463