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  7863  poxp  8140  soxp  8141  tz7.49  8455  omwordri  8580  odi  8587  omass  8588  oewordri  8601  nndi  8632  nnmass  8633  frr3g  9760  r1sdom  9781  tz9.12lem3  9796  cardlim  10053  carduni  10062  alephordi  10153  alephval3  10189  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  axcclem  10535  zorn2lem5  10578  zorn2lem6  10579  axdclem2  10598  alephval2  10657  gruen  10897  grur1a  10904  grothomex  10914  nqereu  11014  distrlem5pr  11112  psslinpr  11116  ltaprlem  11129  suplem1pr  11137  lbreu  12267  fleqceilz  13994  caubnd  15526  divconjdvds  16485  algcvga  16754  algfx  16755  gsummatr01lem3  22972  fiinopn  23219  hausnei  23646  hausnei2  23671  cmpsublem  23717  cmpsub  23718  fcfneii  24356  ppiublem1  27529  sltsun2  28175  nb3grprlem1  29961  cusgrsize2inds  30034  wlk1walk  30219  clwlkclwwlklem2  30591  clwwlkf  30638  clwwlknonwwlknonb  30697  vdgn1frgrv2  30897  frgrncvvdeqlem8  30907  frgrncvvdeqlem9  30908  frgrreggt1  30994  frgrregord013  30996  chintcli  31933  h1datomi  32183  strlem3a  32854  hstrlem3a  32862  mdexchi  32937  cvbr4i  32969  mdsymlem4  33008  mdsymlem6  33010  3jaodd  36480  ifscgr  36809  dfttc4lem2  37317  bj-fvimacnv0  38208  exrecfnlem  38303  wepwsolem  44049  rp-fakeimass  44513  ee233  45502  iccpartgt  48509  lighneal  48696  grlictr  49113  ldepspr  49585