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  elabgt  3685  elabgtOLD  3686  mob  3739  otiunsndisj  5539  sotri2  6161  sotri3  6162  relresfld  6307  limuni3  7889  poxp  8169  soxp  8170  tz7.49  8501  omwordri  8628  odi  8635  omass  8636  oewordri  8648  nndi  8679  nnmass  8680  frr3g  9825  r1sdom  9843  tz9.12lem3  9858  cardlim  10041  carduni  10050  alephordi  10143  alephval3  10179  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  axcclem  10526  zorn2lem5  10569  zorn2lem6  10570  axdclem2  10589  alephval2  10641  gruen  10881  grur1a  10888  grothomex  10898  nqereu  10998  distrlem5pr  11096  psslinpr  11100  ltaprlem  11113  suplem1pr  11121  lbreu  12245  fleqceilz  13905  caubnd  15407  divconjdvds  16363  algcvga  16626  algfx  16627  gsummatr01lem3  22684  fiinopn  22928  hausnei  23357  hausnei2  23382  cmpsublem  23428  cmpsub  23429  fcfneii  24066  ppiublem1  27264  ssltun2  27872  nb3grprlem1  29415  cusgrsize2inds  29489  wlk1walk  29675  clwlkclwwlklem2  30032  clwwlkf  30079  clwwlknonwwlknonb  30138  vdgn1frgrv2  30328  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  frgrreggt1  30425  frgrregord013  30427  chintcli  31363  h1datomi  31613  strlem3a  32284  hstrlem3a  32292  mdexchi  32367  cvbr4i  32399  mdsymlem4  32438  mdsymlem6  32440  3jaodd  35677  ifscgr  36008  bj-fvimacnv0  37252  exrecfnlem  37345  wepwsolem  42999  rp-fakeimass  43474  ee233  44490  iccpartgt  47301  lighneal  47485  grlictr  47832  ldepspr  48202