Theorem com13 79

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 78	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com23 77	1 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  com24  86  an13s  534  an31s  537  funopg  5048  f1o2ndf1  5993  brecop  6382  fiintim  6639  elfz0ubfz0  9536  elfz0fzfz0  9537  fz0fzelfz0  9538  fz0fzdiffz0  9541  fzo1fzo0n0  9594  elfzodifsumelfzo  9612  ssfzo12  9635  ssfzo12bi  9636  facwordi  10148  fihashf1rn  10197  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161  dfgcd2  11281  sqrt2irr  11419  bj-inf2vnlem2  11866