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  1250  rspct  2922  po2nr  4452  funssres  5418  f1ocnv2d  6288  f1o3d  6292  tfrlem9  6584  nnmass  6754  nnmordi  6783  genpcdl  7880  genpcuu  7881  mulnqprl  7929  mulnqpru  7930  distrlem1prl  7943  distrlem1pru  7944  divgt0  9196  divge0  9197  uzind2  9741  facdiv  11159  swrdswrdlem  11459  wrd2ind  11478  dvdsabseq  12597  divgcdcoprm0  12862  lmodvsdi  14631