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  842  3imp231  1112  rexlimdv  3213  sbcimdvOLD  3792  reusv1  5321  reusv2lem3  5324  reusv3  5329  sbcop1  5403  funopsn  7029  isofrlem  7220  oprabidw  7315  oprabid  7316  sorpsscmpl  7596  tfindsg  7716  frxp  7976  poxp  7978  reldmtpos  8059  tfrlem9  8225  tfr3  8239  odi  8419  omass  8420  pssnn  8960  isinf  9045  pssnnOLD  9049  ordiso2  9283  ordtypelem7  9292  preleqg  9382  cantnf  9460  indcardi  9806  dfac2b  9895  cfslb2n  10033  infpssrlem4  10071  axdc4lem  10220  zorn2lem7  10267  fpwwe2lem7  10402  grudomon  10582  distrlem5pr  10792  ltexprlem1  10801  axpre-sup  10934  bndndx  12241  uzind2  12422  elfznelfzo  13501  ssnn0fi  13714  leexp1a  13902  swrdswrdlem  14426  swrdswrd  14427  swrdccat3blem  14461  reuccatpfxs1lem  14468  cncongr1  16381  prm23ge5  16525  unbenlem  16618  infpnlem1  16620  initoeu1  17735  termoeu1  17742  ring1ne0  19839  neindisj2  22283  cmpsub  22560  gausslemma2dlem1a  26522  uhgr2edg  27584  upgrewlkle2  27982  wlklenvclwlkOLD  28032  upgrwlkdvdelem  28113  usgr2pth  28141  wwlksm1edg  28255  frgr3vlem1  28646  3vfriswmgrlem  28650  frgrwopreglem4a  28683  frgrwopreg  28696  shscli  29688  mdbr3  30668  mdbr4  30669  dmdbr3  30676  dmdbr4  30677  mdslmd1i  30700  chjatom  30728  mdsymlem4  30777  cdj3lem2b  30808  bnj517  32874  3jaodd  33666  dfon2lem6  33773  poseq  33811  nocvxminlem  33981  funray  34451  imp5p  34509  bj-cbvalim  34835  bj-cbvexim  34836  bj-fvimacnv0  35466  brabg2  35883  neificl  35920  grpomndo  36042  rngoueqz  36107  subsubelfzo0  44829  fzoopth  44830  2ffzoeq  44831  ztprmneprm  45694