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  5385  f1o2ndf1  6423  brecop  6858  fiintim  7190  elpq  9980  xnn0lenn0nn0  10197  elfz0ubfz0  10458  elfz0fzfz0  10459  fz0fzelfz0  10460  fz0fzdiffz0  10463  fzo1fzo0n0  10521  elfzodifsumelfzo  10545  ssfzo12  10568  ssfzo12bi  10569  facwordi  11101  fihashf1rn  11149  swrdswrdlem  11392  swrdswrd  11393  wrd2ind  11411  swrdccatin1  11413  pfxccatin12lem2  11419  swrdccat  11423  reuccatpfxs1lem  11434  oddnn02np1  12562  oddge22np1  12563  evennn02n  12564  evennn2n  12565  dfgcd2  12706  sqrt2irr  12855  lmodfopnelem1  14464  mpomulcn  15423  zabsle1  15864  gausslemma2dlem1a  15923  2lgsoddprm  15978  upgredg2vtx  16135  usgruspgrben  16173  usgredg2vlem2  16210  edg0usgr  16234  uspgr2wlkeq  16352  clwwlkn1loopb  16407  clwwlkext2edg  16409  clwwlknonex2lem2  16425  bj-inf2vnlem2  16733