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 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))

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  89  com3l  90  com14  97  expd  420  elabgtOLD  3633  mob  3681  otiunsndisj  5505  sotri2  6131  sotri3  6132  relresfld  6279  limuni3  7849  poxp  8125  soxp  8126  tz7.49  8433  omwordri  8558  odi  8565  omass  8566  oewordri  8579  nndi  8610  nnmass  8611  frr3g  9729  r1sdom  9747  tz9.12lem3  9762  cardlim  9959  carduni  9968  alephordi  10059  alephval3  10095  domtriomlem  10427  axdc3lem2  10436  axdc3lem4  10438  axcclem  10442  zorn2lem5  10485  zorn2lem6  10486  axdclem2  10505  alephval2  10558  gruen  10798  grur1a  10805  grothomex  10815  nqereu  10915  distrlem5pr  11013  psslinpr  11017  ltaprlem  11030  suplem1pr  11038  lbreu  12166  fleqceilz  13889  caubnd  15412  divconjdvds  16374  algcvga  16638  algfx  16639  gsummatr01lem3  22795  fiinopn  23039  hausnei  23466  hausnei2  23491  cmpsublem  23537  cmpsub  23538  fcfneii  24175  ppiublem1  27347  sltsun2  27963  nb3grprlem1  29711  cusgrsize2inds  29784  wlk1walk  29969  clwlkclwwlklem2  30332  clwwlkf  30379  clwwlknonwwlknonb  30438  vdgn1frgrv2  30628  frgrncvvdeqlem8  30638  frgrncvvdeqlem9  30639  frgrreggt1  30725  frgrregord013  30727  chintcli  31664  h1datomi  31914  strlem3a  32585  hstrlem3a  32593  mdexchi  32668  cvbr4i  32700  mdsymlem4  32739  mdsymlem6  32741  3jaodd  36188  ifscgr  36517  dfttc4lem2  37021  bj-fvimacnv0  37911  exrecfnlem  38006  wepwsolem  43752  rp-fakeimass  44221  ee233  45211  iccpartgt  48159  lighneal  48346  grlictr  48763  ldepspr  49236