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  5414  f1o2ndf1  6468  brecop  6903  fiintim  7243  elpq  10067  xnn0lenn0nn0  10285  elfz0ubfz0  10550  elfz0fzfz0  10551  fz0fzelfz0  10552  fz0fzdiffz0  10555  fzo1fzo0n0  10613  elfzodifsumelfzo  10637  ssfzo12  10660  ssfzo12bi  10661  facwordi  11201  fihashf1rn  11250  swrdswrdlem  11499  swrdswrd  11500  wrd2ind  11518  swrdccatin1  11520  pfxccatin12lem2  11526  swrdccat  11530  reuccatpfxs1lem  11541  oddnn02np1  12673  oddge22np1  12674  evennn02n  12675  evennn2n  12676  dfgcd2  12817  sqrt2irr  12967  lmodfopnelem1  14771  mpomulcn  15804  zabsle1  16335  gausslemma2dlem1a  16394  2lgsoddprm  16449  upgredg2vtx  16606  usgruspgrben  16644  usgredg2vlem2  16681  edg0usgr  16705  uspgr2wlkeq  16823  clwwlkn1loopb  16878  clwwlkext2edg  16880  clwwlknonex2lem2  16896  bj-inf2vnlem2  17214