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  569  an31s  572  3imp31  1222  3imp21  1224  funopg  5360  f1o2ndf1  6393  brecop  6794  fiintim  7123  elpq  9883  xnn0lenn0nn0  10100  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  fzo1fzo0n0  10423  elfzodifsumelfzo  10447  ssfzo12  10470  ssfzo12bi  10471  facwordi  11003  fihashf1rn  11051  swrdswrdlem  11289  swrdswrd  11290  wrd2ind  11308  swrdccatin1  11310  pfxccatin12lem2  11316  swrdccat  11320  reuccatpfxs1lem  11331  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  dfgcd2  12590  sqrt2irr  12739  lmodfopnelem1  14344  mpomulcn  15296  zabsle1  15734  gausslemma2dlem1a  15793  2lgsoddprm  15848  upgredg2vtx  16005  usgruspgrben  16043  usgredg2vlem2  16080  edg0usgr  16104  uspgr2wlkeq  16222  clwwlkn1loopb  16277  clwwlkext2edg  16279  clwwlknonex2lem2  16295  bj-inf2vnlem2  16592