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  411  a2and  851  3imp231  1118  rexlimdv  3139  reusv1  5333  reusv2lem3  5336  reusv3  5341  sbcop1  5435  funopsnOLD  7098  isofrlem  7291  oprabidw  7394  oprabid  7395  sorpsscmpl  7684  tfindsg  7808  frxp  8073  poxp  8075  poseq  8105  reldmtpos  8181  tfrlem9  8321  tfr3  8335  odi  8511  omass  8512  pssnn  9100  isinf  9172  ordiso2  9427  ordtypelem7  9436  preleqg  9534  cantnf  9612  indcardi  9961  dfac2b  10051  cfslb2n  10188  infpssrlem4  10226  axdc4lem  10375  zorn2lem7  10422  fpwwe2lem7  10558  grudomon  10738  distrlem5pr  10948  ltexprlem1  10957  axpre-sup  11090  bndndx  12434  uzind2  12620  fzoopth  13715  elfznelfzo  13726  ssnn0fi  13945  leexp1a  14135  swrdswrdlem  14664  swrdswrd  14665  swrdccat3blem  14699  reuccatpfxs1lem  14706  cncongr1  16634  prm23ge5  16784  unbenlem  16877  infpnlem1  16879  initoeu1  17976  termoeu1  17983  ring1ne0  20278  neindisj2  23113  cmpsub  23390  gausslemma2dlem1a  27353  nocvxminlem  27771  negsprop  28052  uhgr2edg  29302  upgrewlkle2  29700  upgrwlkdvdelem  29829  usgr2pth  29857  cyclnumvtx  29893  wwlksm1edg  29974  frgr3vlem1  30368  3vfriswmgrlem  30372  frgrwopreglem4a  30405  frgrwopreg  30418  shscli  31413  mdbr3  32393  mdbr4  32394  dmdbr3  32401  dmdbr4  32402  mdslmd1i  32425  chjatom  32453  mdsymlem4  32502  cdj3lem2b  32533  bnj517  35074  3jaodd  35950  dfon2lem6  36021  funray  36375  imp5p  36546  regsfromregtco  36773  bj-fvimacnv0  37653  brabg2  38091  neificl  38127  grpomndo  38249  rngoueqz  38314  relpfrlem  45404  subsubelfzo0  47797  2ffzoeq  47798  ztprmneprm  48845