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  409  a2and  841  3imp231  1111  rexlimdv  3151  sbcimdvOLD  3853  reusv1  5396  reusv2lem3  5399  reusv3  5404  sbcop1  5489  funopsn  7149  isofrlem  7341  oprabidw  7444  oprabid  7445  sorpsscmpl  7728  tfindsg  7854  frxp  8116  poxp  8118  poseq  8148  reldmtpos  8223  tfrlem9  8389  tfr3  8403  odi  8583  omass  8584  pssnn  9172  isinf  9264  isinfOLD  9265  pssnnOLD  9269  ordiso2  9514  ordtypelem7  9523  preleqg  9614  cantnf  9692  indcardi  10040  dfac2b  10129  cfslb2n  10267  infpssrlem4  10305  axdc4lem  10454  zorn2lem7  10501  fpwwe2lem7  10636  grudomon  10816  distrlem5pr  11026  ltexprlem1  11035  axpre-sup  11168  bndndx  12477  uzind2  12661  elfznelfzo  13743  ssnn0fi  13956  leexp1a  14146  swrdswrdlem  14660  swrdswrd  14661  swrdccat3blem  14695  reuccatpfxs1lem  14702  cncongr1  16610  prm23ge5  16754  unbenlem  16847  infpnlem1  16849  initoeu1  17967  termoeu1  17974  ring1ne0  20189  neindisj2  22849  cmpsub  23126  gausslemma2dlem1a  27102  nocvxminlem  27513  negsprop  27746  uhgr2edg  28730  upgrewlkle2  29128  upgrwlkdvdelem  29258  usgr2pth  29286  wwlksm1edg  29400  frgr3vlem1  29791  3vfriswmgrlem  29795  frgrwopreglem4a  29828  frgrwopreg  29841  shscli  30835  mdbr3  31815  mdbr4  31816  dmdbr3  31823  dmdbr4  31824  mdslmd1i  31847  chjatom  31875  mdsymlem4  31924  cdj3lem2b  31955  bnj517  34192  3jaodd  34986  dfon2lem6  35062  funray  35414  imp5p  35501  bj-cbvalim  35827  bj-cbvexim  35828  bj-fvimacnv0  36472  brabg2  36890  neificl  36926  grpomndo  37048  rngoueqz  37113  subsubelfzo0  46334  fzoopth  46335  2ffzoeq  46336  ztprmneprm  47113