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  2900  po2nr  4401  funssres  5363  f1ocnv2d  6219  tfrlem9  6476  nnmass  6646  nnmordi  6675  genpcdl  7722  genpcuu  7723  mulnqprl  7771  mulnqpru  7772  distrlem1prl  7785  distrlem1pru  7786  divgt0  9035  divge0  9036  uzind2  9575  facdiv  10977  swrdswrdlem  11257  wrd2ind  11276  dvdsabseq  12379  divgcdcoprm0  12644  lmodvsdi  14296