Theorem com24 37

Description: Commutation of antecedents. Swap 2nd and 4th.

Hypothesis

Ref	Expression
com4.1	⊢ (φ → (ψ → (χ → (θ → τ))))

Assertion

Ref	Expression
com24	⊢ (φ → (θ → (χ → (ψ → τ))))

Proof of Theorem com24

Step	Hyp	Ref	Expression
1		com4.1	. . . 4 ⊢ (φ → (ψ → (χ → (θ → τ))))
2	1	com34 36	. . 3 ⊢ (φ → (ψ → (θ → (χ → τ))))
3	2	com23 32	. 2 ⊢ (φ → (θ → (ψ → (χ → τ))))
4	3	com34 36	1 ⊢ (φ → (θ → (χ → (ψ → τ))))

Syntax hints:   → wi 2

This theorem is referenced by:  tfrlem5 2953  tfrlem9 2957  tz7.49 2997  omcl 3139  oecl 3140  omordi 3164  nnmcl 3173  nnaordex 3191  nnawordex 3192  fundmen 3333  pssnn 3428  fiint 3445  r1ord 3499  zornlem7 3609  unxpdomlem 3649  genpnnp 3902  prlem934 3933  ltexprlem7 3942  prlem936b 3948  suplem1pr 3955  suppsr2 4017  seqrn 4673  infxpidmlem12 4944  elspansn4t 5478  osumlem4 5533  mdsymlem3 5778  mdsymlem5 5780

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org