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  7886  genpcuu  7887  mulnqprl  7935  mulnqpru  7936  distrlem1prl  7949  distrlem1pru  7950  divgt0  9203  divge0  9204  uzind2  9760  facdiv  11178  swrdswrdlem  11478  wrd2ind  11497  dvdsabseq  12616  divgcdcoprm0  12881  lmodvsdi  14650