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  3672  elabgtOLD  3673  mob  3723  otiunsndisj  5525  sotri2  6149  sotri3  6150  relresfld  6296  limuni3  7873  poxp  8153  soxp  8154  tz7.49  8485  omwordri  8610  odi  8617  omass  8618  oewordri  8630  nndi  8661  nnmass  8662  frr3g  9796  r1sdom  9814  tz9.12lem3  9829  cardlim  10012  carduni  10021  alephordi  10114  alephval3  10150  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  axcclem  10497  zorn2lem5  10540  zorn2lem6  10541  axdclem2  10560  alephval2  10612  gruen  10852  grur1a  10859  grothomex  10869  nqereu  10969  distrlem5pr  11067  psslinpr  11071  ltaprlem  11084  suplem1pr  11092  lbreu  12218  fleqceilz  13894  caubnd  15397  divconjdvds  16352  algcvga  16616  algfx  16617  gsummatr01lem3  22663  fiinopn  22907  hausnei  23336  hausnei2  23361  cmpsublem  23407  cmpsub  23408  fcfneii  24045  ppiublem1  27246  ssltun2  27854  nb3grprlem1  29397  cusgrsize2inds  29471  wlk1walk  29657  clwlkclwwlklem2  30019  clwwlkf  30066  clwwlknonwwlknonb  30125  vdgn1frgrv2  30315  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  frgrreggt1  30412  frgrregord013  30414  chintcli  31350  h1datomi  31600  strlem3a  32271  hstrlem3a  32279  mdexchi  32354  cvbr4i  32386  mdsymlem4  32425  mdsymlem6  32427  3jaodd  35715  ifscgr  36045  bj-fvimacnv0  37287  exrecfnlem  37380  wepwsolem  43054  rp-fakeimass  43525  ee233  44539  iccpartgt  47414  lighneal  47598  grlictr  47975  ldepspr  48390