Theorem com3r 87

Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)

Hypothesis

Ref	Expression
com3.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
com3r	⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))

Proof of Theorem com3r

Step	Hyp	Ref	Expression
1		com3.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com23 86	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	com12 32	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:  com13  88  com3l  89  com14  96  expd  402  expdOLD  403  ad5ant23OLD  765  ad5ant24OLD  767  ad5ant25OLD  769  mob  3593  otiunsndisj  5182  idrefOLD  5727  sotri2  5743  sotri3  5744  relresfld  5883  limuni3  7285  poxp  7526  soxp  7527  tz7.49  7779  omwordri  7892  odi  7899  omass  7900  oewordri  7912  nndi  7943  nnmass  7944  r1sdom  8887  tz9.12lem3  8902  cardlim  9084  carduni  9093  alephordi  9183  alephval3  9219  domtriomlem  9552  axdc3lem2  9561  axdc3lem4  9563  axcclem  9567  zorn2lem5  9610  zorn2lem6  9611  axdclem2  9630  alephval2  9682  gruen  9922  grur1a  9929  grothomex  9939  nqereu  10039  distrlem5pr  10137  psslinpr  10141  ltaprlem  10154  suplem1pr  10162  lbreu  11261  fleqceilz  12880  caubnd  14324  divconjdvds  15263  algcvga  15514  algfx  15515  gsummatr01lem3  20679  fiinopn  20923  hausnei  21350  hausnei2  21375  cmpsublem  21420  cmpsub  21421  fcfneii  22058  ppiublem1  25147  nb3grprlem1  26504  cusgrsize2inds  26583  wlk1walk  26769  clwlkclwwlklem2  27149  clwwlkf  27202  vdgn1frgrv2  27477  frgrncvvdeqlem8  27487  frgrncvvdeqlem9  27488  frgrreggt1  27587  frgrregord013  27589  chintcli  28524  h1datomi  28774  strlem3a  29445  hstrlem3a  29453  mdexchi  29528  cvbr4i  29560  mdsymlem4  29599  mdsymlem6  29601  3jaodd  31922  frr3g  32105  ifscgr  32477  bj-mo3OLD  33147  wepwsolem  38114  rp-fakeimass  38358  ee233  39224  iccpartgt  41939  lighneal  42104  ldepspr  42831