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  3167  reusv1  5373  reusv2lem3  5376  reusv3  5381  sbcop1  5475  funopsnOLD  7152  isofrlem  7349  oprabidw  7454  oprabid  7455  sorpsscmpl  7744  tfindsg  7866  frxp  8131  poxp  8133  poseq  8163  reldmtpos  8239  tfrlem9  8381  tfr3  8395  odi  8573  omass  8574  pssnn  9163  isinf  9235  ordiso2  9487  ordtypelem7  9496  preleqg  9594  cantnf  9672  indcardi  10044  dfac2b  10133  cfslb2n  10270  infpssrlem4  10308  axdc4lem  10457  zorn2lem7  10504  fpwwe2lem7  10640  grudomon  10820  distrlem5pr  11030  ltexprlem1  11039  axpre-sup  11172  bndndx  12521  uzind2  12707  fzoopth  13810  elfznelfzo  13821  ssnn0fi  14041  leexp1a  14231  swrdswrdlem  14765  swrdswrd  14766  swrdccat3blem  14800  reuccatpfxs1lem  14807  cncongr1  16750  prm23ge5  16900  unbenlem  16993  infpnlem1  16995  initoeu1  18093  termoeu1  18100  ring1ne0  20415  neindisj2  23317  cmpsub  23594  gausslemma2dlem1a  27566  nocvxminlem  27984  negsprop  28265  uhgr2edg  29595  upgrewlkle2  29993  upgrwlkdvdelem  30122  usgr2pth  30150  cyclnumvtx  30186  wwlksm1edg  30267  frgr3vlem1  30661  3vfriswmgrlem  30665  frgrwopreglem4a  30698  frgrwopreg  30711  shscli  31706  mdbr3  32686  mdbr4  32687  dmdbr3  32694  dmdbr4  32695  mdslmd1i  32718  chjatom  32746  mdsymlem4  32795  cdj3lem2b  32826  bnj517  35304  3jaodd  36227  dfon2lem6  36298  funray  36652  imp5p  36863  regsfromregtco  37089  bj-fvimacnv0  37970  brabg2  38408  neificl  38444  grpomndo  38566  rngoueqz  38631  relpfrlem  45702  subsubelfzo0  48104  2ffzoeq  48105  ztprmneprm  49167