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  5355  f1o2ndf1  6385  brecop  6785  fiintim  7109  elpq  9861  xnn0lenn0nn0  10078  elfz0ubfz0  10338  elfz0fzfz0  10339  fz0fzelfz0  10340  fz0fzdiffz0  10343  fzo1fzo0n0  10400  elfzodifsumelfzo  10424  ssfzo12  10447  ssfzo12bi  10448  facwordi  10979  fihashf1rn  11027  swrdswrdlem  11257  swrdswrd  11258  wrd2ind  11276  swrdccatin1  11278  pfxccatin12lem2  11284  swrdccat  11288  reuccatpfxs1lem  11299  oddnn02np1  12412  oddge22np1  12413  evennn02n  12414  evennn2n  12415  dfgcd2  12556  sqrt2irr  12705  lmodfopnelem1  14309  mpomulcn  15261  zabsle1  15699  gausslemma2dlem1a  15758  2lgsoddprm  15813  upgredg2vtx  15967  usgruspgrben  16005  usgredg2vlem2  16042  edg0usgr  16066  uspgr2wlkeq  16137  clwwlkn1loopb  16188  clwwlkext2edg  16190  bj-inf2vnlem2  16443