Theorem com3l 81

Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)

Hypothesis

Ref	Expression
com3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
com3l	⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Proof of Theorem com3l

Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3r 79	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com3r 79	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  impd  254  3imp231  1221  expdcom  1485  nebidc  2480  sbcimdv  3095  prel12  3852  reusv3  4555  relcoi1  5266  oprabid  6045  poxp  6392  reldmtpos  6414  tfrlem9  6480  tfri3  6528  ordiso2  7228  distrlem5prl  7799  distrlem5pru  7800  bndndx  9394  uzind2  9585  leexp1a  10849  swrdswrdlem  11278  swrdswrd  11279  swrdccat3blem  11313  reuccatpfxs1lem  11320  cncongr1  12668  infpnlem1  12925  gausslemma2dlem1a  15780  uhgr2edg  16050  bj-inf2vnlem2  16516