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  419  elabgtOLD  3632  mob  3679  otiunsndisj  5488  sotri2  6113  sotri3  6114  relresfld  6259  limuni3  7828  poxp  8103  soxp  8104  tz7.49  8411  omwordri  8536  odi  8543  omass  8544  oewordri  8557  nndi  8588  nnmass  8589  frr3g  9711  r1sdom  9729  tz9.12lem3  9744  cardlim  9927  carduni  9936  alephordi  10027  alephval3  10063  domtriomlem  10396  axdc3lem2  10405  axdc3lem4  10407  axcclem  10411  zorn2lem5  10454  zorn2lem6  10455  axdclem2  10474  alephval2  10527  gruen  10767  grur1a  10774  grothomex  10784  nqereu  10884  distrlem5pr  10982  psslinpr  10986  ltaprlem  10999  suplem1pr  11007  lbreu  12139  fleqceilz  13861  caubnd  15369  divconjdvds  16332  algcvga  16596  algfx  16597  gsummatr01lem3  22697  fiinopn  22941  hausnei  23368  hausnei2  23393  cmpsublem  23439  cmpsub  23440  fcfneii  24077  ppiublem1  27243  sltsun2  27859  nb3grprlem1  29527  cusgrsize2inds  29600  wlk1walk  29785  clwlkclwwlklem2  30148  clwwlkf  30195  clwwlknonwwlknonb  30254  vdgn1frgrv2  30444  frgrncvvdeqlem8  30454  frgrncvvdeqlem9  30455  frgrreggt1  30541  frgrregord013  30543  chintcli  31480  h1datomi  31730  strlem3a  32401  hstrlem3a  32409  mdexchi  32484  cvbr4i  32516  mdsymlem4  32555  mdsymlem6  32557  3jaodd  36029  ifscgr  36358  dfttc4lem2  36853  bj-fvimacnv0  37742  exrecfnlem  37837  wepwsolem  43583  rp-fakeimass  44052  ee233  45059  iccpartgt  47997  lighneal  48184  grlictr  48601  ldepspr  49059