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  4454  funssres  5420  f1ocnv2d  6294  f1o3d  6298  tfrlem9  6590  nnmass  6760  nnmordi  6789  genpcdl  7887  genpcuu  7888  mulnqprl  7936  mulnqpru  7937  distrlem1prl  7950  distrlem1pru  7951  divgt0  9205  divge0  9206  uzind2  9763  facdiv  11191  swrdswrdlem  11491  wrd2ind  11510  dvdsabseq  12632  divgcdcoprm0  12897  lmodvsdi  14699