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  417  elabgt  3663  mob  3714  otiunsndisj  5521  sotri2  6131  sotri3  6132  relresfld  6276  limuni3  7841  poxp  8114  soxp  8115  tz7.49  8445  omwordri  8572  odi  8579  omass  8580  oewordri  8592  nndi  8623  nnmass  8624  frr3g  9751  r1sdom  9769  tz9.12lem3  9784  cardlim  9967  carduni  9976  alephordi  10069  alephval3  10105  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  axcclem  10452  zorn2lem5  10495  zorn2lem6  10496  axdclem2  10515  alephval2  10567  gruen  10807  grur1a  10814  grothomex  10824  nqereu  10924  distrlem5pr  11022  psslinpr  11026  ltaprlem  11039  suplem1pr  11047  lbreu  12164  fleqceilz  13819  caubnd  15305  divconjdvds  16258  algcvga  16516  algfx  16517  gsummatr01lem3  22159  fiinopn  22403  hausnei  22832  hausnei2  22857  cmpsublem  22903  cmpsub  22904  fcfneii  23541  ppiublem1  26705  ssltun2  27311  nb3grprlem1  28668  cusgrsize2inds  28741  wlk1walk  28927  clwlkclwwlklem2  29284  clwwlkf  29331  clwwlknonwwlknonb  29390  vdgn1frgrv2  29580  frgrncvvdeqlem8  29590  frgrncvvdeqlem9  29591  frgrreggt1  29677  frgrregord013  29679  chintcli  30615  h1datomi  30865  strlem3a  31536  hstrlem3a  31544  mdexchi  31619  cvbr4i  31651  mdsymlem4  31690  mdsymlem6  31692  3jaodd  34715  ifscgr  35047  bj-fvimacnv0  36215  exrecfnlem  36308  wepwsolem  41832  rp-fakeimass  42311  ee233  43328  iccpartgt  46143  lighneal  46327  ldepspr  47202