Theorem com34 83

Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem com34

Step	Hyp	Ref	Expression
1		com4.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2		pm2.04 82	. 2 ⊢ ((𝜒 → (𝜃 → 𝜏)) → (𝜃 → (𝜒 → 𝜏)))
3	1, 2	syl6 33	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:  com4l  84  com35  90  3an1rs  1243  rspct  2901  po2nr  4404  funssres  5366  f1ocnv2d  6222  tfrlem9  6480  nnmass  6650  nnmordi  6679  genpcdl  7732  genpcuu  7733  mulnqprl  7781  mulnqpru  7782  distrlem1prl  7795  distrlem1pru  7796  divgt0  9045  divge0  9046  uzind2  9585  facdiv  10993  swrdswrdlem  11278  wrd2ind  11297  dvdsabseq  12401  divgcdcoprm0  12666  lmodvsdi  14318