Theorem com3l 90

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 88	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))
3	2	com3r 88	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  93  impd  415  a2and  858  3imp231  1128  rexlimdv  3164  reusv1  5359  reusv2lem3  5362  reusv3  5367  sbcop1  5461  funopsnOLD  7135  isofrlem  7328  oprabidw  7431  oprabid  7432  sorpsscmpl  7721  tfindsg  7845  frxp  8110  poxp  8112  poseq  8142  reldmtpos  8218  tfrlem9  8360  tfr3  8374  odi  8552  omass  8553  pssnn  9141  isinf  9213  ordiso2  9465  ordtypelem7  9474  preleqg  9572  cantnf  9650  indcardi  10013  dfac2b  10102  cfslb2n  10240  infpssrlem4  10278  axdc4lem  10427  zorn2lem7  10474  fpwwe2lem7  10610  grudomon  10790  distrlem5pr  11000  ltexprlem1  11009  axpre-sup  11142  bndndx  12494  uzind2  12680  fzoopth  13782  elfznelfzo  13793  ssnn0fi  14012  leexp1a  14202  swrdswrdlem  14731  swrdswrd  14732  swrdccat3blem  14766  reuccatpfxs1lem  14773  cncongr1  16715  prm23ge5  16865  unbenlem  16958  infpnlem1  16960  initoeu1  18058  termoeu1  18065  ring1ne0  20373  neindisj2  23241  cmpsub  23518  gausslemma2dlem1a  27487  nocvxminlem  27905  negsprop  28186  uhgr2edg  29467  upgrewlkle2  29865  upgrwlkdvdelem  29994  usgr2pth  30022  cyclnumvtx  30058  wwlksm1edg  30139  frgr3vlem1  30533  3vfriswmgrlem  30537  frgrwopreglem4a  30570  frgrwopreg  30583  shscli  31578  mdbr3  32558  mdbr4  32559  dmdbr3  32566  dmdbr4  32567  mdslmd1i  32590  chjatom  32618  mdsymlem4  32667  cdj3lem2b  32698  bnj517  35190  3jaodd  36078  dfon2lem6  36149  funray  36503  imp5p  36684  regsfromregtco  36911  bj-fvimacnv0  37790  brabg2  38228  neificl  38264  grpomndo  38386  rngoueqz  38451  relpfrlem  45527  subsubelfzo0  47919  2ffzoeq  47920  ztprmneprm  48978