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  556  an31s  559  funopg  5152  f1o2ndf1  6118  brecop  6512  fiintim  6810  xnn0lenn0nn0  9641  elfz0ubfz0  9895  elfz0fzfz0  9896  fz0fzelfz0  9897  fz0fzdiffz0  9900  fzo1fzo0n0  9953  elfzodifsumelfzo  9971  ssfzo12  9994  ssfzo12bi  9995  facwordi  10479  fihashf1rn  10528  oddnn02np1  11566  oddge22np1  11567  evennn02n  11568  evennn2n  11569  dfgcd2  11691  sqrt2irr  11829  bj-inf2vnlem2  13158