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  10060  xnn0lenn0nn0  10278  elfz0ubfz0  10543  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  fzo1fzo0n0  10606  elfzodifsumelfzo  10630  ssfzo12  10653  ssfzo12bi  10654  facwordi  11193  fihashf1rn  11242  swrdswrdlem  11491  swrdswrd  11492  wrd2ind  11510  swrdccatin1  11512  pfxccatin12lem2  11518  swrdccat  11522  reuccatpfxs1lem  11533  oddnn02np1  12665  oddge22np1  12666  evennn02n  12667  evennn2n  12668  dfgcd2  12809  sqrt2irr  12959  lmodfopnelem1  14712  mpomulcn  15719  zabsle1  16240  gausslemma2dlem1a  16299  2lgsoddprm  16354  upgredg2vtx  16511  usgruspgrben  16549  usgredg2vlem2  16586  edg0usgr  16610  uspgr2wlkeq  16728  clwwlkn1loopb  16783  clwwlkext2edg  16785  clwwlknonex2lem2  16801  bj-inf2vnlem2  17119