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  1245  rspct  2903  po2nr  4406  funssres  5369  f1ocnv2d  6227  tfrlem9  6485  nnmass  6655  nnmordi  6684  genpcdl  7739  genpcuu  7740  mulnqprl  7788  mulnqpru  7789  distrlem1prl  7802  distrlem1pru  7803  divgt0  9052  divge0  9053  uzind2  9592  facdiv  11001  swrdswrdlem  11289  wrd2ind  11308  dvdsabseq  12413  divgcdcoprm0  12678  lmodvsdi  14331