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 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com24  87  an13s  573  an31s  576  3imp31  1227  3imp21  1229  funopg  5411  f1o2ndf1  6464  brecop  6899  fiintim  7238  elpq  10051  xnn0lenn0nn0  10269  elfz0ubfz0  10534  elfz0fzfz0  10535  fz0fzelfz0  10536  fz0fzdiffz0  10539  fzo1fzo0n0  10597  elfzodifsumelfzo  10621  ssfzo12  10644  ssfzo12bi  10645  facwordi  11180  fihashf1rn  11229  swrdswrdlem  11478  swrdswrd  11479  wrd2ind  11497  swrdccatin1  11499  pfxccatin12lem2  11505  swrdccat  11509  reuccatpfxs1lem  11520  oddnn02np1  12649  oddge22np1  12650  evennn02n  12651  evennn2n  12652  dfgcd2  12793  sqrt2irr  12942  lmodfopnelem1  14663  mpomulcn  15669  zabsle1  16130  gausslemma2dlem1a  16189  2lgsoddprm  16244  upgredg2vtx  16401  usgruspgrben  16439  usgredg2vlem2  16476  edg0usgr  16500  uspgr2wlkeq  16618  clwwlkn1loopb  16673  clwwlkext2edg  16675  clwwlknonex2lem2  16691  bj-inf2vnlem2  17009