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  410  a2and  845  3imp231  1112  rexlimdv  3135  reusv1  5342  reusv2lem3  5345  reusv3  5350  sbcop1  5436  funopsn  7093  isofrlem  7286  oprabidw  7389  oprabid  7390  sorpsscmpl  7679  tfindsg  7803  frxp  8068  poxp  8070  poseq  8100  reldmtpos  8176  tfrlem9  8316  tfr3  8330  odi  8506  omass  8507  pssnn  9093  isinf  9165  ordiso2  9420  ordtypelem7  9429  preleqg  9524  cantnf  9602  indcardi  9951  dfac2b  10041  cfslb2n  10178  infpssrlem4  10216  axdc4lem  10365  zorn2lem7  10412  fpwwe2lem7  10548  grudomon  10728  distrlem5pr  10938  ltexprlem1  10947  axpre-sup  11080  bndndx  12400  uzind2  12585  fzoopth  13678  elfznelfzo  13689  ssnn0fi  13908  leexp1a  14098  swrdswrdlem  14627  swrdswrd  14628  swrdccat3blem  14662  reuccatpfxs1lem  14669  cncongr1  16594  prm23ge5  16743  unbenlem  16836  infpnlem1  16838  initoeu1  17935  termoeu1  17942  ring1ne0  20234  neindisj2  23067  cmpsub  23344  gausslemma2dlem1a  27332  nocvxminlem  27750  negsprop  28031  uhgr2edg  29281  upgrewlkle2  29680  upgrwlkdvdelem  29809  usgr2pth  29837  cyclnumvtx  29873  wwlksm1edg  29954  frgr3vlem1  30348  3vfriswmgrlem  30352  frgrwopreglem4a  30385  frgrwopreg  30398  shscli  31392  mdbr3  32372  mdbr4  32373  dmdbr3  32380  dmdbr4  32381  mdslmd1i  32404  chjatom  32432  mdsymlem4  32481  cdj3lem2b  32512  bnj517  35041  3jaodd  35909  dfon2lem6  35980  funray  36334  imp5p  36505  regsfromregtr  36668  bj-cbvalim  36845  bj-cbvexim  36846  bj-fvimacnv0  37487  brabg2  37914  neificl  37950  grpomndo  38072  rngoueqz  38137  relpfrlem  45190  subsubelfzo0  47568  2ffzoeq  47569  ztprmneprm  48589