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  4364  funssres  5322  f1ocnv2d  6163  tfrlem9  6418  nnmass  6586  nnmordi  6615  genpcdl  7652  genpcuu  7653  mulnqprl  7701  mulnqpru  7702  distrlem1prl  7715  distrlem1pru  7716  divgt0  8965  divge0  8966  uzind2  9505  facdiv  10905  swrdswrdlem  11180  wrd2ind  11199  dvdsabseq  12233  divgcdcoprm0  12498  lmodvsdi  14148