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  1199  3imp21  1201  funopg  5313  f1o2ndf1  6326  brecop  6724  fiintim  7042  elpq  9785  xnn0lenn0nn0  10002  elfz0ubfz0  10262  elfz0fzfz0  10263  fz0fzelfz0  10264  fz0fzdiffz0  10267  fzo1fzo0n0  10324  elfzodifsumelfzo  10347  ssfzo12  10370  ssfzo12bi  10371  facwordi  10902  fihashf1rn  10950  swrdswrdlem  11175  swrdswrd  11176  wrd2ind  11194  oddnn02np1  12261  oddge22np1  12262  evennn02n  12263  evennn2n  12264  dfgcd2  12405  sqrt2irr  12554  lmodfopnelem1  14156  mpomulcn  15108  zabsle1  15546  gausslemma2dlem1a  15605  2lgsoddprm  15660  bj-inf2vnlem2  16041