Theorem com24 87

Description: Commutation of antecedents. Swap 2nd and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com24	⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → 𝜏))))

Proof of Theorem com24

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4t 85	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com13 80	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:  com25  91  tfrlem9  6528  nnmordi  6727  fundmen  7024  fiintim  7166  elfzodifsumelfzo  10492  ssfzo12  10515  swrdswrdlem  11334  swrdswrd  11335  wrd2ind  11353  swrdccatin1  11355  dvdsmodexp  12419  dvdsaddre2b  12465  infpnlem1  12995  grpinveu  13684  mulgass2  14135  lss1d  14462  cnpnei  15013  clwwlkccatlem  16324