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 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  84  com35  90  3an1rs  1250  rspct  2922  po2nr  4456  funssres  5423  f1ocnv2d  6297  f1o3d  6301  tfrlem9  6594  nnmass  6764  nnmordi  6793  genpcdl  7893  genpcuu  7894  mulnqprl  7942  mulnqpru  7943  distrlem1prl  7956  distrlem1pru  7957  divgt0  9211  divge0  9212  uzind2  9770  facdiv  11199  swrdswrdlem  11499  wrd2ind  11518  dvdsabseq  12640  divgcdcoprm0  12905  lmodvsdi  14758