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  3639  elabgtOLDOLD  3640  mob  3688  otiunsndisj  5480  sotri2  6102  sotri3  6103  relresfld  6249  limuni3  7828  poxp  8107  soxp  8108  tz7.49  8413  omwordri  8536  odi  8543  omass  8544  oewordri  8556  nndi  8587  nnmass  8588  frr3g  9709  r1sdom  9727  tz9.12lem3  9742  cardlim  9925  carduni  9934  alephordi  10027  alephval3  10063  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axcclem  10410  zorn2lem5  10453  zorn2lem6  10454  axdclem2  10473  alephval2  10525  gruen  10765  grur1a  10772  grothomex  10782  nqereu  10882  distrlem5pr  10980  psslinpr  10984  ltaprlem  10997  suplem1pr  11005  lbreu  12133  fleqceilz  13816  caubnd  15325  divconjdvds  16285  algcvga  16549  algfx  16550  gsummatr01lem3  22544  fiinopn  22788  hausnei  23215  hausnei2  23240  cmpsublem  23286  cmpsub  23287  fcfneii  23924  ppiublem1  27113  ssltun2  27721  nb3grprlem1  29307  cusgrsize2inds  29381  wlk1walk  29567  clwlkclwwlklem2  29929  clwwlkf  29976  clwwlknonwwlknonb  30035  vdgn1frgrv2  30225  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  frgrreggt1  30322  frgrregord013  30324  chintcli  31260  h1datomi  31510  strlem3a  32181  hstrlem3a  32189  mdexchi  32264  cvbr4i  32296  mdsymlem4  32335  mdsymlem6  32337  3jaodd  35702  ifscgr  36032  bj-fvimacnv0  37274  exrecfnlem  37367  wepwsolem  43031  rp-fakeimass  43501  ee233  44509  iccpartgt  47428  lighneal  47612  grlictr  48007  ldepspr  48462