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  4400  funssres  5360  f1ocnv2d  6216  tfrlem9  6471  nnmass  6641  nnmordi  6670  genpcdl  7714  genpcuu  7715  mulnqprl  7763  mulnqpru  7764  distrlem1prl  7777  distrlem1pru  7778  divgt0  9027  divge0  9028  uzind2  9567  facdiv  10968  swrdswrdlem  11244  wrd2ind  11263  dvdsabseq  12366  divgcdcoprm0  12631  lmodvsdi  14283