Theorem com3l 89

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 87	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com3r 87	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  92  impd  414  a2and  856  3imp231  1124  rexlimdv  3160  reusv1  5353  reusv2lem3  5356  reusv3  5361  sbcop1  5455  funopsnOLD  7127  isofrlem  7320  oprabidw  7423  oprabid  7424  sorpsscmpl  7713  tfindsg  7837  frxp  8101  poxp  8103  poseq  8133  reldmtpos  8209  tfrlem9  8351  tfr3  8365  odi  8543  omass  8544  pssnn  9133  isinf  9205  ordiso2  9460  ordtypelem7  9469  preleqg  9567  cantnf  9645  indcardi  9994  dfac2b  10084  cfslb2n  10222  infpssrlem4  10260  axdc4lem  10409  zorn2lem7  10456  fpwwe2lem7  10592  grudomon  10772  distrlem5pr  10982  ltexprlem1  10991  axpre-sup  11124  bndndx  12477  uzind2  12663  fzoopth  13765  elfznelfzo  13776  ssnn0fi  13995  leexp1a  14185  swrdswrdlem  14714  swrdswrd  14715  swrdccat3blem  14749  reuccatpfxs1lem  14756  cncongr1  16684  prm23ge5  16834  unbenlem  16927  infpnlem1  16929  initoeu1  18027  termoeu1  18034  ring1ne0  20328  neindisj2  23163  cmpsub  23440  gausslemma2dlem1a  27406  nocvxminlem  27824  negsprop  28105  uhgr2edg  29355  upgrewlkle2  29753  upgrwlkdvdelem  29882  usgr2pth  29910  cyclnumvtx  29946  wwlksm1edg  30027  frgr3vlem1  30421  3vfriswmgrlem  30425  frgrwopreglem4a  30458  frgrwopreg  30471  shscli  31466  mdbr3  32446  mdbr4  32447  dmdbr3  32454  dmdbr4  32455  mdslmd1i  32478  chjatom  32506  mdsymlem4  32555  cdj3lem2b  32586  bnj517  35144  3jaodd  36029  dfon2lem6  36100  funray  36454  imp5p  36635  regsfromregtco  36862  bj-fvimacnv0  37742  brabg2  38180  neificl  38216  grpomndo  38338  rngoueqz  38403  relpfrlem  45493  subsubelfzo0  47885  2ffzoeq  47886  ztprmneprm  48933