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  elabgtOLD  3615  elabgtOLDOLD  3616  mob  3663  otiunsndisj  5474  sotri2  6092  sotri3  6093  relresfld  6240  limuni3  7803  poxp  8078  soxp  8079  tz7.49  8384  omwordri  8507  odi  8514  omass  8515  oewordri  8528  nndi  8559  nnmass  8560  frr3g  9680  r1sdom  9698  tz9.12lem3  9713  cardlim  9896  carduni  9905  alephordi  9996  alephval3  10032  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axcclem  10379  zorn2lem5  10422  zorn2lem6  10423  axdclem2  10442  alephval2  10495  gruen  10735  grur1a  10742  grothomex  10752  nqereu  10852  distrlem5pr  10950  psslinpr  10954  ltaprlem  10967  suplem1pr  10975  lbreu  12106  fleqceilz  13813  caubnd  15321  divconjdvds  16284  algcvga  16548  algfx  16549  gsummatr01lem3  22622  fiinopn  22866  hausnei  23293  hausnei2  23318  cmpsublem  23364  cmpsub  23365  fcfneii  24002  ppiublem1  27165  sltsun2  27781  nb3grprlem1  29449  cusgrsize2inds  29522  wlk1walk  29707  clwlkclwwlklem2  30070  clwwlkf  30117  clwwlknonwwlknonb  30176  vdgn1frgrv2  30366  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  frgrreggt1  30463  frgrregord013  30465  chintcli  31402  h1datomi  31652  strlem3a  32323  hstrlem3a  32331  mdexchi  32406  cvbr4i  32438  mdsymlem4  32477  mdsymlem6  32479  3jaodd  35897  ifscgr  36226  dfttc4lem2  36711  bj-fvimacnv0  37600  exrecfnlem  37695  wepwsolem  43470  rp-fakeimass  43939  ee233  44946  iccpartgt  47887  lighneal  48074  grlictr  48491  ldepspr  48949