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  415  elabgtOLD  3624  elabgtOLDOLD  3625  mob  3672  otiunsndisj  5463  sotri2  6080  sotri3  6081  relresfld  6228  limuni3  7788  poxp  8064  soxp  8065  tz7.49  8370  omwordri  8493  odi  8500  omass  8501  oewordri  8513  nndi  8544  nnmass  8545  frr3g  9656  r1sdom  9674  tz9.12lem3  9689  cardlim  9872  carduni  9881  alephordi  9972  alephval3  10008  domtriomlem  10340  axdc3lem2  10349  axdc3lem4  10351  axcclem  10355  zorn2lem5  10398  zorn2lem6  10399  axdclem2  10418  alephval2  10470  gruen  10710  grur1a  10717  grothomex  10727  nqereu  10827  distrlem5pr  10925  psslinpr  10929  ltaprlem  10942  suplem1pr  10950  lbreu  12079  fleqceilz  13760  caubnd  15268  divconjdvds  16228  algcvga  16492  algfx  16493  gsummatr01lem3  22573  fiinopn  22817  hausnei  23244  hausnei2  23269  cmpsublem  23315  cmpsub  23316  fcfneii  23953  ppiublem1  27141  ssltun2  27751  nb3grprlem1  29360  cusgrsize2inds  29434  wlk1walk  29619  clwlkclwwlklem2  29982  clwwlkf  30029  clwwlknonwwlknonb  30088  vdgn1frgrv2  30278  frgrncvvdeqlem8  30288  frgrncvvdeqlem9  30289  frgrreggt1  30375  frgrregord013  30377  chintcli  31313  h1datomi  31563  strlem3a  32234  hstrlem3a  32242  mdexchi  32317  cvbr4i  32349  mdsymlem4  32388  mdsymlem6  32390  3jaodd  35780  ifscgr  36109  bj-fvimacnv0  37351  exrecfnlem  37444  wepwsolem  43160  rp-fakeimass  43630  ee233  44637  iccpartgt  47552  lighneal  47736  grlictr  48140  ldepspr  48599