Theorem com3r 88

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 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	com12 33	1 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com13  89  com3l  90  com14  97  expd  421  elabgtOLD  3627  mob  3675  otiunsndisj  5493  sotri2  6121  sotri3  6122  relresfldOLD  6272  limuni3  7852  poxp  8129  soxp  8130  tz7.49  8439  omwordri  8564  odi  8571  omass  8572  oewordri  8585  nndi  8616  nnmass  8617  frr3g  9744  r1sdom  9764  tz9.12lem3  9779  cardlim  10034  carduni  10043  alephordi  10134  alephval3  10170  domtriomlem  10501  axdc3lem2  10510  axdc3lem4  10512  axcclem  10516  zorn2lem5  10559  zorn2lem6  10560  axdclem2  10579  alephval2  10638  gruen  10878  grur1a  10885  grothomex  10895  nqereu  10995  distrlem5pr  11093  psslinpr  11097  ltaprlem  11110  suplem1pr  11118  lbreu  12248  fleqceilz  13974  caubnd  15506  divconjdvds  16465  algcvga  16734  algfx  16735  gsummatr01lem3  22952  fiinopn  23199  hausnei  23626  hausnei2  23651  cmpsublem  23697  cmpsub  23698  fcfneii  24336  ppiublem1  27511  sltsun2  28157  nb3grprlem1  29943  cusgrsize2inds  30016  wlk1walk  30201  clwlkclwwlklem2  30573  clwwlkf  30620  clwwlknonwwlknonb  30679  vdgn1frgrv2  30879  frgrncvvdeqlem8  30889  frgrncvvdeqlem9  30890  frgrreggt1  30976  frgrregord013  30978  chintcli  31915  h1datomi  32165  strlem3a  32836  hstrlem3a  32844  mdexchi  32919  cvbr4i  32951  mdsymlem4  32990  mdsymlem6  32992  3jaodd  36449  ifscgr  36779  dfttc4lem2  37287  bj-fvimacnv0  38175  exrecfnlem  38270  wepwsolem  44002  rp-fakeimass  44471  ee233  45461  iccpartgt  48453  lighneal  48640  grlictr  49057  ldepspr  49529