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  5358  f1o2ndf1  6388  brecop  6789  fiintim  7118  elpq  9876  xnn0lenn0nn0  10093  elfz0ubfz0  10353  elfz0fzfz0  10354  fz0fzelfz0  10355  fz0fzdiffz0  10358  fzo1fzo0n0  10415  elfzodifsumelfzo  10439  ssfzo12  10462  ssfzo12bi  10463  facwordi  10995  fihashf1rn  11043  swrdswrdlem  11278  swrdswrd  11279  wrd2ind  11297  swrdccatin1  11299  pfxccatin12lem2  11305  swrdccat  11309  reuccatpfxs1lem  11320  oddnn02np1  12434  oddge22np1  12435  evennn02n  12436  evennn2n  12437  dfgcd2  12578  sqrt2irr  12727  lmodfopnelem1  14331  mpomulcn  15283  zabsle1  15721  gausslemma2dlem1a  15780  2lgsoddprm  15835  upgredg2vtx  15992  usgruspgrben  16030  usgredg2vlem2  16067  edg0usgr  16091  uspgr2wlkeq  16176  clwwlkn1loopb  16229  clwwlkext2edg  16231  clwwlknonex2lem2  16247  bj-inf2vnlem2  16516