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  1223  3imp21  1225  funopg  5367  f1o2ndf1  6402  brecop  6837  fiintim  7166  elpq  9926  xnn0lenn0nn0  10143  elfz0ubfz0  10403  elfz0fzfz0  10404  fz0fzelfz0  10405  fz0fzdiffz0  10408  fzo1fzo0n0  10466  elfzodifsumelfzo  10490  ssfzo12  10513  ssfzo12bi  10514  facwordi  11046  fihashf1rn  11094  swrdswrdlem  11332  swrdswrd  11333  wrd2ind  11351  swrdccatin1  11353  pfxccatin12lem2  11359  swrdccat  11363  reuccatpfxs1lem  11374  oddnn02np1  12502  oddge22np1  12503  evennn02n  12504  evennn2n  12505  dfgcd2  12646  sqrt2irr  12795  lmodfopnelem1  14400  mpomulcn  15357  zabsle1  15798  gausslemma2dlem1a  15857  2lgsoddprm  15912  upgredg2vtx  16069  usgruspgrben  16107  usgredg2vlem2  16144  edg0usgr  16168  uspgr2wlkeq  16286  clwwlkn1loopb  16341  clwwlkext2edg  16343  clwwlknonex2lem2  16359  bj-inf2vnlem2  16667