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  1222  rspct  2874  po2nr  4363  funssres  5321  f1ocnv2d  6162  tfrlem9  6417  nnmass  6585  nnmordi  6614  genpcdl  7647  genpcuu  7648  mulnqprl  7696  mulnqpru  7697  distrlem1prl  7710  distrlem1pru  7711  divgt0  8960  divge0  8961  uzind2  9500  facdiv  10900  swrdswrdlem  11175  wrd2ind  11194  dvdsabseq  12228  divgcdcoprm0  12493  lmodvsdi  14143