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  4397  funssres  5356  f1ocnv2d  6200  tfrlem9  6455  nnmass  6623  nnmordi  6652  genpcdl  7694  genpcuu  7695  mulnqprl  7743  mulnqpru  7744  distrlem1prl  7757  distrlem1pru  7758  divgt0  9007  divge0  9008  uzind2  9547  facdiv  10947  swrdswrdlem  11222  wrd2ind  11241  dvdsabseq  12344  divgcdcoprm0  12609  lmodvsdi  14260