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  1246  rspct  2904  po2nr  4412  funssres  5376  f1ocnv2d  6237  tfrlem9  6528  nnmass  6698  nnmordi  6727  genpcdl  7782  genpcuu  7783  mulnqprl  7831  mulnqpru  7832  distrlem1prl  7845  distrlem1pru  7846  divgt0  9095  divge0  9096  uzind2  9635  facdiv  11044  swrdswrdlem  11332  wrd2ind  11351  dvdsabseq  12469  divgcdcoprm0  12734  lmodvsdi  14387