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  1220  3imp21  1222  funopg  5352  f1o2ndf1  6380  brecop  6780  fiintim  7101  elpq  9852  xnn0lenn0nn0  10069  elfz0ubfz0  10329  elfz0fzfz0  10330  fz0fzelfz0  10331  fz0fzdiffz0  10334  fzo1fzo0n0  10391  elfzodifsumelfzo  10415  ssfzo12  10438  ssfzo12bi  10439  facwordi  10970  fihashf1rn  11018  swrdswrdlem  11244  swrdswrd  11245  wrd2ind  11263  swrdccatin1  11265  pfxccatin12lem2  11271  swrdccat  11275  reuccatpfxs1lem  11286  oddnn02np1  12399  oddge22np1  12400  evennn02n  12401  evennn2n  12402  dfgcd2  12543  sqrt2irr  12692  lmodfopnelem1  14296  mpomulcn  15248  zabsle1  15686  gausslemma2dlem1a  15745  2lgsoddprm  15800  upgredg2vtx  15954  usgruspgrben  15992  usgredg2vlem2  16029  uspgr2wlkeq  16086  bj-inf2vnlem2  16358