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 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com4l  93  impd  416  a2and  859  3imp231  1130  rexlimdv  3162  reusv1  5359  reusv2lem3  5362  reusv3  5367  sbcop1  5458  funopsnOLD  7144  isofrlem  7340  oprabidw  7443  oprabid  7444  sorpsscmpl  7739  tfindsg  7861  frxp  8127  poxp  8129  poseq  8159  reldmtpos  8235  tfrlem9  8377  tfr3  8391  odi  8571  omass  8572  pssnn  9168  isinf  9240  ordiso2  9493  ordtypelem7  9502  preleqg  9600  cantnf  9678  indcardi  10101  dfac2b  10190  cfslb2n  10327  infpssrlem4  10365  axdc4lem  10514  zorn2lem7  10561  fpwwe2lem7  10703  grudomon  10883  distrlem5pr  11093  ltexprlem1  11102  axpre-sup  11235  bndndx  12586  uzind2  12773  fzoopth  13877  elfznelfzo  13888  ssnn0fi  14108  leexp1a  14298  swrdswrdlem  14833  swrdswrd  14834  swrdccat3blem  14868  reuccatpfxs1lem  14875  cncongr1  16822  prm23ge5  16973  unbenlem  17066  infpnlem1  17068  initoeu1  18166  termoeu1  18173  ring1ne0  20510  neindisj2  23421  cmpsub  23698  gausslemma2dlem1a  27674  nocvxminlem  28122  negsprop  28403  uhgr2edg  29771  upgrewlkle2  30169  upgrwlkdvdelem  30304  usgr2pth  30332  cyclnumvtx  30370  wwlksm1edg  30452  frgr3vlem1  30856  3vfriswmgrlem  30860  frgrwopreglem4a  30893  frgrwopreg  30906  shscli  31901  mdbr3  32881  mdbr4  32882  dmdbr3  32889  dmdbr4  32890  mdslmd1i  32913  chjatom  32941  mdsymlem4  32990  cdj3lem2b  33021  bnj517  35498  3jaodd  36449  dfon2lem6  36520  funray  36875  imp5p  37070  regsfromregtco  37296  bj-fvimacnv0  38175  brabg2  38619  neificl  38655  grpomndo  38777  rngoueqz  38842  relpfrlem  45895  subsubelfzo0  48341  2ffzoeq  48342  ztprmneprm  49403