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 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  84  impd  254  3imp231  1228  expdcom  1492  nebidc  2500  sbcimdv  3117  prel12  3896  reusv3  4606  relcoi1  5319  oprabid  6117  poxp  6468  reldmtpos  6524  tfrlem9  6590  tfri3  6638  ordiso2  7375  distrlem5prl  7953  distrlem5pru  7954  bndndx  9564  uzind2  9760  leexp1a  11033  swrdswrdlem  11478  swrdswrd  11479  swrdccat3blem  11513  reuccatpfxs1lem  11520  cncongr1  12883  infpnlem1  13140  gausslemma2dlem1a  16189  uhgr2edg  16459  lealltlt1  16763  bj-inf2vnlem2  17009