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  2913  po2nr  4429  funssres  5394  f1ocnv2d  6258  tfrlem9  6549  nnmass  6719  nnmordi  6748  genpcdl  7833  genpcuu  7834  mulnqprl  7882  mulnqpru  7883  distrlem1prl  7896  distrlem1pru  7897  divgt0  9145  divge0  9146  uzind2  9689  facdiv  11099  swrdswrdlem  11392  wrd2ind  11411  dvdsabseq  12529  divgcdcoprm0  12794  lmodvsdi  14451