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  569  an31s  572  3imp31  1223  3imp21  1225  funopg  5391  f1o2ndf1  6437  brecop  6872  fiintim  7204  elpq  10002  xnn0lenn0nn0  10220  elfz0ubfz0  10484  elfz0fzfz0  10485  fz0fzelfz0  10486  fz0fzdiffz0  10489  fzo1fzo0n0  10547  elfzodifsumelfzo  10571  ssfzo12  10594  ssfzo12bi  10595  facwordi  11130  fihashf1rn  11179  swrdswrdlem  11424  swrdswrd  11425  wrd2ind  11443  swrdccatin1  11445  pfxccatin12lem2  11451  swrdccat  11455  reuccatpfxs1lem  11466  oddnn02np1  12595  oddge22np1  12596  evennn02n  12597  evennn2n  12598  dfgcd2  12739  sqrt2irr  12888  lmodfopnelem1  14602  mpomulcn  15561  zabsle1  16002  gausslemma2dlem1a  16061  2lgsoddprm  16116  upgredg2vtx  16273  usgruspgrben  16311  usgredg2vlem2  16348  edg0usgr  16372  uspgr2wlkeq  16490  clwwlkn1loopb  16545  clwwlkext2edg  16547  clwwlknonex2lem2  16563  bj-inf2vnlem2  16881