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  3635  mob  3683  otiunsndisj  5508  sotri2  6134  sotri3  6135  relresfldOLD  6284  limuni3  7857  poxp  8133  soxp  8134  tz7.49  8441  omwordri  8566  odi  8573  omass  8574  oewordri  8587  nndi  8618  nnmass  8619  frr3g  9738  r1sdom  9756  tz9.12lem3  9771  cardlim  9977  carduni  9986  alephordi  10077  alephval3  10113  domtriomlem  10444  axdc3lem2  10453  axdc3lem4  10455  axcclem  10459  zorn2lem5  10502  zorn2lem6  10503  axdclem2  10522  alephval2  10575  gruen  10815  grur1a  10822  grothomex  10832  nqereu  10932  distrlem5pr  11030  psslinpr  11034  ltaprlem  11047  suplem1pr  11055  lbreu  12183  fleqceilz  13907  caubnd  15436  divconjdvds  16398  algcvga  16662  algfx  16663  gsummatr01lem3  22851  fiinopn  23095  hausnei  23522  hausnei2  23547  cmpsublem  23593  cmpsub  23594  fcfneii  24231  ppiublem1  27403  sltsun2  28019  nb3grprlem1  29767  cusgrsize2inds  29840  wlk1walk  30025  clwlkclwwlklem2  30388  clwwlkf  30435  clwwlknonwwlknonb  30494  vdgn1frgrv2  30684  frgrncvvdeqlem8  30694  frgrncvvdeqlem9  30695  frgrreggt1  30781  frgrregord013  30783  chintcli  31720  h1datomi  31970  strlem3a  32641  hstrlem3a  32649  mdexchi  32724  cvbr4i  32756  mdsymlem4  32795  mdsymlem6  32797  3jaodd  36228  ifscgr  36557  dfttc4lem2  37081  bj-fvimacnv0  37971  exrecfnlem  38066  wepwsolem  43810  rp-fakeimass  44279  ee233  45269  iccpartgt  48217  lighneal  48404  grlictr  48821  ldepspr  49294