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  mob  3649  otiunsndisj  5308  sotri2  5872  sotri3  5873  relresfld  6009  limuni3  7430  poxp  7682  soxp  7683  tz7.49  7939  omwordri  8055  odi  8062  omass  8063  oewordri  8075  nndi  8106  nnmass  8107  r1sdom  9056  tz9.12lem3  9071  cardlim  9254  carduni  9263  alephordi  9353  alephval3  9389  domtriomlem  9717  axdc3lem2  9726  axdc3lem4  9728  axcclem  9732  zorn2lem5  9775  zorn2lem6  9776  axdclem2  9795  alephval2  9847  gruen  10087  grur1a  10094  grothomex  10104  nqereu  10204  distrlem5pr  10302  psslinpr  10306  ltaprlem  10319  suplem1pr  10327  lbreu  11445  fleqceilz  13076  caubnd  14556  divconjdvds  15502  algcvga  15756  algfx  15757  gsummatr01lem3  20954  fiinopn  21197  hausnei  21624  hausnei2  21649  cmpsublem  21695  cmpsub  21696  fcfneii  22333  ppiublem1  25464  nb3grprlem1  26849  cusgrsize2inds  26922  wlk1walk  27107  clwlkclwwlklem2  27464  clwwlkf  27512  vdgn1frgrv2  27763  frgrncvvdeqlem8  27773  frgrncvvdeqlem9  27774  frgrreggt1  27860  frgrregord013  27862  chintcli  28795  h1datomi  29045  strlem3a  29716  hstrlem3a  29724  mdexchi  29799  cvbr4i  29831  mdsymlem4  29870  mdsymlem6  29872  3jaodd  32554  frr3g  32732  ifscgr  33116  exrecfnlem  34212  wepwsolem  39148  rp-fakeimass  39384  ee233  40413  iccpartgt  43091  lighneal  43280  ldepspr  44030