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  3651  elabgtOLD  3652  mob  3700  otiunsndisj  5495  sotri2  6118  sotri3  6119  relresfld  6265  limuni3  7847  poxp  8127  soxp  8128  tz7.49  8459  omwordri  8584  odi  8591  omass  8592  oewordri  8604  nndi  8635  nnmass  8636  frr3g  9770  r1sdom  9788  tz9.12lem3  9803  cardlim  9986  carduni  9995  alephordi  10088  alephval3  10124  domtriomlem  10456  axdc3lem2  10465  axdc3lem4  10467  axcclem  10471  zorn2lem5  10514  zorn2lem6  10515  axdclem2  10534  alephval2  10586  gruen  10826  grur1a  10833  grothomex  10843  nqereu  10943  distrlem5pr  11041  psslinpr  11045  ltaprlem  11058  suplem1pr  11066  lbreu  12192  fleqceilz  13871  caubnd  15377  divconjdvds  16334  algcvga  16598  algfx  16599  gsummatr01lem3  22595  fiinopn  22839  hausnei  23266  hausnei2  23291  cmpsublem  23337  cmpsub  23338  fcfneii  23975  ppiublem1  27165  ssltun2  27773  nb3grprlem1  29359  cusgrsize2inds  29433  wlk1walk  29619  clwlkclwwlklem2  29981  clwwlkf  30028  clwwlknonwwlknonb  30087  vdgn1frgrv2  30277  frgrncvvdeqlem8  30287  frgrncvvdeqlem9  30288  frgrreggt1  30374  frgrregord013  30376  chintcli  31312  h1datomi  31562  strlem3a  32233  hstrlem3a  32241  mdexchi  32316  cvbr4i  32348  mdsymlem4  32387  mdsymlem6  32389  3jaodd  35732  ifscgr  36062  bj-fvimacnv0  37304  exrecfnlem  37397  wepwsolem  43066  rp-fakeimass  43536  ee233  44544  iccpartgt  47441  lighneal  47625  grlictr  48020  ldepspr  48449