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  416  elabgt  3661  mob  3712  otiunsndisj  5519  sotri2  6127  sotri3  6128  relresfld  6272  limuni3  7837  poxp  8110  soxp  8111  tz7.49  8441  omwordri  8568  odi  8575  omass  8576  oewordri  8588  nndi  8619  nnmass  8620  frr3g  9747  r1sdom  9765  tz9.12lem3  9780  cardlim  9963  carduni  9972  alephordi  10065  alephval3  10101  domtriomlem  10433  axdc3lem2  10442  axdc3lem4  10444  axcclem  10448  zorn2lem5  10491  zorn2lem6  10492  axdclem2  10511  alephval2  10563  gruen  10803  grur1a  10810  grothomex  10820  nqereu  10920  distrlem5pr  11018  psslinpr  11022  ltaprlem  11035  suplem1pr  11043  lbreu  12160  fleqceilz  13815  caubnd  15301  divconjdvds  16254  algcvga  16512  algfx  16513  gsummatr01lem3  22150  fiinopn  22394  hausnei  22823  hausnei2  22848  cmpsublem  22894  cmpsub  22895  fcfneii  23532  ppiublem1  26694  ssltun2  27299  nb3grprlem1  28626  cusgrsize2inds  28699  wlk1walk  28885  clwlkclwwlklem2  29242  clwwlkf  29289  clwwlknonwwlknonb  29348  vdgn1frgrv2  29538  frgrncvvdeqlem8  29548  frgrncvvdeqlem9  29549  frgrreggt1  29635  frgrregord013  29637  chintcli  30571  h1datomi  30821  strlem3a  31492  hstrlem3a  31500  mdexchi  31575  cvbr4i  31607  mdsymlem4  31646  mdsymlem6  31648  3jaodd  34672  ifscgr  35004  bj-fvimacnv0  36155  exrecfnlem  36248  wepwsolem  41769  rp-fakeimass  42248  ee233  43265  iccpartgt  46081  lighneal  46265  ldepspr  47107