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  414  elabgt  3659  elabgtOLD  3660  mob  3711  otiunsndisj  5526  sotri2  6141  sotri3  6142  relresfld  6287  limuni3  7862  poxp  8142  soxp  8143  tz7.49  8475  omwordri  8602  odi  8609  omass  8610  oewordri  8622  nndi  8653  nnmass  8654  frr3g  9799  r1sdom  9817  tz9.12lem3  9832  cardlim  10015  carduni  10024  alephordi  10117  alephval3  10153  domtriomlem  10485  axdc3lem2  10494  axdc3lem4  10496  axcclem  10500  zorn2lem5  10543  zorn2lem6  10544  axdclem2  10563  alephval2  10615  gruen  10855  grur1a  10862  grothomex  10872  nqereu  10972  distrlem5pr  11070  psslinpr  11074  ltaprlem  11087  suplem1pr  11095  lbreu  12216  fleqceilz  13874  caubnd  15363  divconjdvds  16317  algcvga  16580  algfx  16581  gsummatr01lem3  22650  fiinopn  22894  hausnei  23323  hausnei2  23348  cmpsublem  23394  cmpsub  23395  fcfneii  24032  ppiublem1  27231  ssltun2  27839  nb3grprlem1  29316  cusgrsize2inds  29390  wlk1walk  29576  clwlkclwwlklem2  29933  clwwlkf  29980  clwwlknonwwlknonb  30039  vdgn1frgrv2  30229  frgrncvvdeqlem8  30239  frgrncvvdeqlem9  30240  frgrreggt1  30326  frgrregord013  30328  chintcli  31264  h1datomi  31514  strlem3a  32185  hstrlem3a  32193  mdexchi  32268  cvbr4i  32300  mdsymlem4  32339  mdsymlem6  32341  3jaodd  35537  ifscgr  35868  bj-fvimacnv0  36993  exrecfnlem  37086  wepwsolem  42703  rp-fakeimass  43179  ee233  44195  iccpartgt  46999  lighneal  47183  grlictr  47505  ldepspr  47856