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  3671  elabgtOLD  3672  mob  3725  otiunsndisj  5529  sotri2  6151  sotri3  6152  relresfld  6297  limuni3  7872  poxp  8151  soxp  8152  tz7.49  8483  omwordri  8608  odi  8615  omass  8616  oewordri  8628  nndi  8659  nnmass  8660  frr3g  9793  r1sdom  9811  tz9.12lem3  9826  cardlim  10009  carduni  10018  alephordi  10111  alephval3  10147  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  axcclem  10494  zorn2lem5  10537  zorn2lem6  10538  axdclem2  10557  alephval2  10609  gruen  10849  grur1a  10856  grothomex  10866  nqereu  10966  distrlem5pr  11064  psslinpr  11068  ltaprlem  11081  suplem1pr  11089  lbreu  12215  fleqceilz  13890  caubnd  15393  divconjdvds  16348  algcvga  16612  algfx  16613  gsummatr01lem3  22678  fiinopn  22922  hausnei  23351  hausnei2  23376  cmpsublem  23422  cmpsub  23423  fcfneii  24060  ppiublem1  27260  ssltun2  27868  nb3grprlem1  29411  cusgrsize2inds  29485  wlk1walk  29671  clwlkclwwlklem2  30028  clwwlkf  30075  clwwlknonwwlknonb  30134  vdgn1frgrv2  30324  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  frgrreggt1  30421  frgrregord013  30423  chintcli  31359  h1datomi  31609  strlem3a  32280  hstrlem3a  32288  mdexchi  32363  cvbr4i  32395  mdsymlem4  32434  mdsymlem6  32436  3jaodd  35694  ifscgr  36025  bj-fvimacnv0  37268  exrecfnlem  37361  wepwsolem  43030  rp-fakeimass  43501  ee233  44516  iccpartgt  47351  lighneal  47535  grlictr  47910  ldepspr  48318