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  5348  f1o2ndf1  6364  brecop  6762  fiintim  7081  elpq  9832  xnn0lenn0nn0  10049  elfz0ubfz0  10309  elfz0fzfz0  10310  fz0fzelfz0  10311  fz0fzdiffz0  10314  fzo1fzo0n0  10371  elfzodifsumelfzo  10394  ssfzo12  10417  ssfzo12bi  10418  facwordi  10949  fihashf1rn  10997  swrdswrdlem  11222  swrdswrd  11223  wrd2ind  11241  swrdccatin1  11243  pfxccatin12lem2  11249  swrdccat  11253  reuccatpfxs1lem  11264  oddnn02np1  12377  oddge22np1  12378  evennn02n  12379  evennn2n  12380  dfgcd2  12521  sqrt2irr  12670  lmodfopnelem1  14273  mpomulcn  15225  zabsle1  15663  gausslemma2dlem1a  15722  2lgsoddprm  15777  upgredg2vtx  15931  usgruspgrben  15969  usgredg2vlem2  16006  bj-inf2vnlem2  16264