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

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  93  impd  415  a2and  858  3imp231  1130  rexlimdv  3164  reusv1  5370  reusv2lem3  5373  reusv3  5378  sbcop1  5472  funopsnOLD  7147  isofrlem  7340  oprabidw  7443  oprabid  7444  sorpsscmpl  7733  tfindsg  7858  frxp  8123  poxp  8125  poseq  8155  reldmtpos  8231  tfrlem9  8373  tfr3  8387  odi  8565  omass  8566  pssnn  9154  isinf  9226  ordiso2  9478  ordtypelem7  9487  preleqg  9585  cantnf  9663  indcardi  10026  dfac2b  10115  cfslb2n  10253  infpssrlem4  10291  axdc4lem  10440  zorn2lem7  10487  fpwwe2lem7  10623  grudomon  10803  distrlem5pr  11013  ltexprlem1  11022  axpre-sup  11155  bndndx  12504  uzind2  12690  fzoopth  13793  elfznelfzo  13804  ssnn0fi  14023  leexp1a  14213  swrdswrdlem  14743  swrdswrd  14744  swrdccat3blem  14778  reuccatpfxs1lem  14785  cncongr1  16726  prm23ge5  16876  unbenlem  16969  infpnlem1  16971  initoeu1  18069  termoeu1  18076  ring1ne0  20383  neindisj2  23261  cmpsub  23538  gausslemma2dlem1a  27507  nocvxminlem  27925  negsprop  28206  uhgr2edg  29536  upgrewlkle2  29934  upgrwlkdvdelem  30063  usgr2pth  30091  cyclnumvtx  30127  wwlksm1edg  30208  frgr3vlem1  30602  3vfriswmgrlem  30606  frgrwopreglem4a  30639  frgrwopreg  30652  shscli  31647  mdbr3  32627  mdbr4  32628  dmdbr3  32635  dmdbr4  32636  mdslmd1i  32659  chjatom  32687  mdsymlem4  32736  cdj3lem2b  32767  bnj517  35251  3jaodd  36185  dfon2lem6  36256  funray  36610  imp5p  36801  regsfromregtco  37027  bj-fvimacnv0  37908  brabg2  38346  neificl  38382  grpomndo  38504  rngoueqz  38569  relpfrlem  45642  subsubelfzo0  48041  2ffzoeq  48042  ztprmneprm  49104