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  11192  swrdswrdlem  11492  wrd2ind  11511  dvdsabseq  12633  divgcdcoprm0  12898  lmodvsdi  14700