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  6480  nnmordi  6679  fundmen  6976  fiintim  7116  elfzodifsumelfzo  10436  ssfzo12  10459  swrdswrdlem  11275  swrdswrd  11276  wrd2ind  11294  swrdccatin1  11296  dvdsmodexp  12346  dvdsaddre2b  12392  infpnlem1  12922  grpinveu  13611  mulgass2  14061  lss1d  14387  cnpnei  14933  clwwlkccatlem  16195