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  1246  rspct  2916  po2nr  4435  funssres  5400  f1ocnv2d  6267  f1o3d  6271  tfrlem9  6563  nnmass  6733  nnmordi  6762  genpcdl  7850  genpcuu  7851  mulnqprl  7899  mulnqpru  7900  distrlem1prl  7913  distrlem1pru  7914  divgt0  9166  divge0  9167  uzind2  9711  facdiv  11128  swrdswrdlem  11424  wrd2ind  11443  dvdsabseq  12562  divgcdcoprm0  12827  lmodvsdi  14589