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  3629  elabgtOLDOLD  3630  mob  3677  otiunsndisj  5476  sotri2  6094  sotri3  6095  relresfld  6242  limuni3  7804  poxp  8080  soxp  8081  tz7.49  8386  omwordri  8509  odi  8516  omass  8517  oewordri  8530  nndi  8561  nnmass  8562  frr3g  9680  r1sdom  9698  tz9.12lem3  9713  cardlim  9896  carduni  9905  alephordi  9996  alephval3  10032  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axcclem  10379  zorn2lem5  10422  zorn2lem6  10423  axdclem2  10442  alephval2  10495  gruen  10735  grur1a  10742  grothomex  10752  nqereu  10852  distrlem5pr  10950  psslinpr  10954  ltaprlem  10967  suplem1pr  10975  lbreu  12104  fleqceilz  13786  caubnd  15294  divconjdvds  16254  algcvga  16518  algfx  16519  gsummatr01lem3  22613  fiinopn  22857  hausnei  23284  hausnei2  23309  cmpsublem  23355  cmpsub  23356  fcfneii  23993  ppiublem1  27181  sltsun2  27797  nb3grprlem1  29465  cusgrsize2inds  29539  wlk1walk  29724  clwlkclwwlklem2  30087  clwwlkf  30134  clwwlknonwwlknonb  30193  vdgn1frgrv2  30383  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  frgrreggt1  30480  frgrregord013  30482  chintcli  31418  h1datomi  31668  strlem3a  32339  hstrlem3a  32347  mdexchi  32422  cvbr4i  32454  mdsymlem4  32493  mdsymlem6  32495  3jaodd  35928  ifscgr  36257  bj-fvimacnv0  37538  exrecfnlem  37631  wepwsolem  43396  rp-fakeimass  43865  ee233  44872  iccpartgt  47784  lighneal  47968  grlictr  48372  ldepspr  48830