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  557  an31s  560  funopg  5165  f1o2ndf1  6133  brecop  6527  fiintim  6825  elpq  9467  xnn0lenn0nn0  9678  elfz0ubfz0  9933  elfz0fzfz0  9934  fz0fzelfz0  9935  fz0fzdiffz0  9938  fzo1fzo0n0  9991  elfzodifsumelfzo  10009  ssfzo12  10032  ssfzo12bi  10033  facwordi  10518  fihashf1rn  10567  oddnn02np1  11613  oddge22np1  11614  evennn02n  11615  evennn2n  11616  dfgcd2  11738  sqrt2irr  11876  bj-inf2vnlem2  13340