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  846  3imp231  1113  rexlimdv  3137  reusv1  5344  reusv2lem3  5347  reusv3  5352  sbcop1  5444  funopsn  7103  isofrlem  7296  oprabidw  7399  oprabid  7400  sorpsscmpl  7689  tfindsg  7813  frxp  8078  poxp  8080  poseq  8110  reldmtpos  8186  tfrlem9  8326  tfr3  8340  odi  8516  omass  8517  pssnn  9105  isinf  9177  ordiso2  9432  ordtypelem7  9441  preleqg  9536  cantnf  9614  indcardi  9963  dfac2b  10053  cfslb2n  10190  infpssrlem4  10228  axdc4lem  10377  zorn2lem7  10424  fpwwe2lem7  10560  grudomon  10740  distrlem5pr  10950  ltexprlem1  10959  axpre-sup  11092  bndndx  12412  uzind2  12597  fzoopth  13690  elfznelfzo  13701  ssnn0fi  13920  leexp1a  14110  swrdswrdlem  14639  swrdswrd  14640  swrdccat3blem  14674  reuccatpfxs1lem  14681  cncongr1  16606  prm23ge5  16755  unbenlem  16848  infpnlem1  16850  initoeu1  17947  termoeu1  17954  ring1ne0  20246  neindisj2  23079  cmpsub  23356  gausslemma2dlem1a  27344  nocvxminlem  27762  negsprop  28043  uhgr2edg  29293  upgrewlkle2  29692  upgrwlkdvdelem  29821  usgr2pth  29849  cyclnumvtx  29885  wwlksm1edg  29966  frgr3vlem1  30360  3vfriswmgrlem  30364  frgrwopreglem4a  30397  frgrwopreg  30410  shscli  31404  mdbr3  32384  mdbr4  32385  dmdbr3  32392  dmdbr4  32393  mdslmd1i  32416  chjatom  32444  mdsymlem4  32493  cdj3lem2b  32524  bnj517  35060  3jaodd  35928  dfon2lem6  35999  funray  36353  imp5p  36524  regsfromregtr  36687  bj-cbvalim  36883  bj-cbvexim  36884  bj-fvimacnv0  37535  brabg2  37962  neificl  37998  grpomndo  38120  rngoueqz  38185  relpfrlem  45303  subsubelfzo0  47680  2ffzoeq  47681  ztprmneprm  48701