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  3630  mob  3678  otiunsndisj  5501  sotri2  6127  sotri3  6128  relresfldOLD  6278  limuni3  7852  poxp  8130  soxp  8131  tz7.49  8438  omwordri  8563  odi  8570  omass  8571  oewordri  8584  nndi  8615  nnmass  8616  frr3g  9742  r1sdom  9760  tz9.12lem3  9775  cardlim  9981  carduni  9990  alephordi  10081  alephval3  10117  domtriomlem  10448  axdc3lem2  10457  axdc3lem4  10459  axcclem  10463  zorn2lem5  10506  zorn2lem6  10507  axdclem2  10526  alephval2  10585  gruen  10825  grur1a  10832  grothomex  10842  nqereu  10942  distrlem5pr  11040  psslinpr  11044  ltaprlem  11057  suplem1pr  11065  lbreu  12193  fleqceilz  13919  caubnd  15450  divconjdvds  16411  algcvga  16675  algfx  16676  gsummatr01lem3  22885  fiinopn  23132  hausnei  23559  hausnei2  23584  cmpsublem  23630  cmpsub  23631  fcfneii  24269  ppiublem1  27446  sltsun2  28062  nb3grprlem1  29848  cusgrsize2inds  29921  wlk1walk  30106  clwlkclwwlklem2  30478  clwwlkf  30525  clwwlknonwwlknonb  30584  vdgn1frgrv2  30784  frgrncvvdeqlem8  30794  frgrncvvdeqlem9  30795  frgrreggt1  30881  frgrregord013  30883  chintcli  31820  h1datomi  32070  strlem3a  32741  hstrlem3a  32749  mdexchi  32824  cvbr4i  32856  mdsymlem4  32895  mdsymlem6  32897  3jaodd  36302  ifscgr  36632  dfttc4lem2  37156  bj-fvimacnv0  38046  exrecfnlem  38141  wepwsolem  43891  rp-fakeimass  44360  ee233  45350  iccpartgt  48335  lighneal  48522  grlictr  48939  ldepspr  49411