Theorem com3r 88

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 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	com12 33	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  89  com3l  90  com14  97  expd  420  elabgtOLD  3635  mob  3683  otiunsndisj  5493  sotri2  6119  sotri3  6120  relresfld  6266  limuni3  7836  poxp  8112  soxp  8113  tz7.49  8420  omwordri  8545  odi  8552  omass  8553  oewordri  8566  nndi  8597  nnmass  8598  frr3g  9716  r1sdom  9734  tz9.12lem3  9749  cardlim  9946  carduni  9955  alephordi  10046  alephval3  10082  domtriomlem  10414  axdc3lem2  10423  axdc3lem4  10425  axcclem  10429  zorn2lem5  10472  zorn2lem6  10473  axdclem2  10492  alephval2  10545  gruen  10785  grur1a  10792  grothomex  10802  nqereu  10902  distrlem5pr  11000  psslinpr  11004  ltaprlem  11017  suplem1pr  11025  lbreu  12153  fleqceilz  13875  caubnd  15398  divconjdvds  16361  algcvga  16625  algfx  16626  gsummatr01lem3  22771  fiinopn  23015  hausnei  23442  hausnei2  23467  cmpsublem  23513  cmpsub  23514  fcfneii  24151  ppiublem1  27320  sltsun2  27936  nb3grprlem1  29635  cusgrsize2inds  29708  wlk1walk  29893  clwlkclwwlklem2  30256  clwwlkf  30303  clwwlknonwwlknonb  30362  vdgn1frgrv2  30552  frgrncvvdeqlem8  30562  frgrncvvdeqlem9  30563  frgrreggt1  30649  frgrregord013  30651  chintcli  31588  h1datomi  31838  strlem3a  32509  hstrlem3a  32517  mdexchi  32592  cvbr4i  32624  mdsymlem4  32663  mdsymlem6  32665  3jaodd  36073  ifscgr  36402  dfttc4lem2  36897  bj-fvimacnv0  37785  exrecfnlem  37880  wepwsolem  43626  rp-fakeimass  44095  ee233  45087  iccpartgt  48032  lighneal  48219  grlictr  48636  ldepspr  49105