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  3626  mob  3674  otiunsndisj  5492  sotri2  6122  sotri3  6123  relresfldOLD  6279  limuni3  7864  poxp  8143  soxp  8144  tz7.49  8459  omwordri  8584  odi  8591  omass  8592  oewordri  8605  nndi  8636  nnmass  8637  frr3g  9764  r1sdom  9785  tz9.12lem3  9800  cardlim  10057  carduni  10066  alephordi  10157  alephval3  10193  domtriomlem  10524  axdc3lem2  10533  axdc3lem4  10535  axcclem  10539  zorn2lem5  10582  zorn2lem6  10583  axdclem2  10602  alephval2  10661  gruen  10901  grur1a  10908  grothomex  10918  nqereu  11018  distrlem5pr  11116  psslinpr  11120  ltaprlem  11133  suplem1pr  11141  lbreu  12271  fleqceilz  13998  caubnd  15532  divconjdvds  16491  algcvga  16760  algfx  16761  gsummatr01lem3  22978  fiinopn  23225  hausnei  23652  hausnei2  23677  cmpsublem  23723  cmpsub  23724  fcfneii  24362  ppiublem1  27535  sltsun2  28181  nb3grprlem1  29967  cusgrsize2inds  30040  wlk1walk  30225  clwlkclwwlklem2  30597  clwwlkf  30644  clwwlknonwwlknonb  30703  vdgn1frgrv2  30903  frgrncvvdeqlem8  30913  frgrncvvdeqlem9  30914  frgrreggt1  31000  frgrregord013  31002  chintcli  31939  h1datomi  32189  strlem3a  32860  hstrlem3a  32868  mdexchi  32943  cvbr4i  32975  mdsymlem4  33014  mdsymlem6  33016  3jaodd  36573  ifscgr  36902  dfttc4lem2  37410  bj-fvimacnv0  38301  exrecfnlem  38396  wepwsolem  44143  rp-fakeimass  44607  ee233  45596  iccpartgt  48603  lighneal  48790  grlictr  49207  ldepspr  49679