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  5356  f1o2ndf1  6386  brecop  6787  fiintim  7114  elpq  9871  xnn0lenn0nn0  10088  elfz0ubfz0  10348  elfz0fzfz0  10349  fz0fzelfz0  10350  fz0fzdiffz0  10353  fzo1fzo0n0  10410  elfzodifsumelfzo  10434  ssfzo12  10457  ssfzo12bi  10458  facwordi  10990  fihashf1rn  11038  swrdswrdlem  11272  swrdswrd  11273  wrd2ind  11291  swrdccatin1  11293  pfxccatin12lem2  11299  swrdccat  11303  reuccatpfxs1lem  11314  oddnn02np1  12428  oddge22np1  12429  evennn02n  12430  evennn2n  12431  dfgcd2  12572  sqrt2irr  12721  lmodfopnelem1  14325  mpomulcn  15277  zabsle1  15715  gausslemma2dlem1a  15774  2lgsoddprm  15829  upgredg2vtx  15983  usgruspgrben  16021  usgredg2vlem2  16058  edg0usgr  16082  uspgr2wlkeq  16153  clwwlkn1loopb  16205  clwwlkext2edg  16207  clwwlknonex2lem2  16223  bj-inf2vnlem2  16476