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  27310  nb3grprlem1  28637  cusgrsize2inds  28710  wlk1walk  28896  clwlkclwwlklem2  29253  clwwlkf  29300  clwwlknonwwlknonb  29359  vdgn1frgrv2  29549  frgrncvvdeqlem8  29559  frgrncvvdeqlem9  29560  frgrreggt1  29646  frgrregord013  29648  chintcli  30584  h1datomi  30834  strlem3a  31505  hstrlem3a  31513  mdexchi  31588  cvbr4i  31620  mdsymlem4  31659  mdsymlem6  31661  3jaodd  34684  ifscgr  35016  bj-fvimacnv0  36167  exrecfnlem  36260  wepwsolem  41784  rp-fakeimass  42263  ee233  43280  iccpartgt  46095  lighneal  46279  ldepspr  47154