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  1224  expdcom  1488  nebidc  2492  sbcimdv  3107  prel12  3874  reusv3  4580  relcoi1  5293  oprabid  6081  poxp  6427  reldmtpos  6483  tfrlem9  6549  tfri3  6597  ordiso2  7325  distrlem5prl  7897  distrlem5pru  7898  bndndx  9491  uzind2  9686  leexp1a  10952  swrdswrdlem  11389  swrdswrd  11390  swrdccat3blem  11424  reuccatpfxs1lem  11431  cncongr1  12793  infpnlem1  13050  gausslemma2dlem1a  15918  uhgr2edg  16188  bj-inf2vnlem2  16728