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  573  an31s  576  3imp31  1227  3imp21  1229  funopg  5409  f1o2ndf1  6458  brecop  6893  fiintim  7232  elpq  10032  xnn0lenn0nn0  10250  elfz0ubfz0  10515  elfz0fzfz0  10516  fz0fzelfz0  10517  fz0fzdiffz0  10520  fzo1fzo0n0  10578  elfzodifsumelfzo  10602  ssfzo12  10625  ssfzo12bi  10626  facwordi  11161  fihashf1rn  11210  swrdswrdlem  11459  swrdswrd  11460  wrd2ind  11478  swrdccatin1  11480  pfxccatin12lem2  11486  swrdccat  11490  reuccatpfxs1lem  11501  oddnn02np1  12630  oddge22np1  12631  evennn02n  12632  evennn2n  12633  dfgcd2  12774  sqrt2irr  12923  lmodfopnelem1  14644  mpomulcn  15650  zabsle1  16101  gausslemma2dlem1a  16160  2lgsoddprm  16215  upgredg2vtx  16372  usgruspgrben  16410  usgredg2vlem2  16447  edg0usgr  16471  uspgr2wlkeq  16589  clwwlkn1loopb  16644  clwwlkext2edg  16646  clwwlknonex2lem2  16662  bj-inf2vnlem2  16980