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  elabgtOLD  3616  elabgtOLDOLD  3617  mob  3664  otiunsndisj  5468  sotri2  6086  sotri3  6087  relresfld  6234  limuni3  7796  poxp  8071  soxp  8072  tz7.49  8377  omwordri  8500  odi  8507  omass  8508  oewordri  8521  nndi  8552  nnmass  8553  frr3g  9671  r1sdom  9689  tz9.12lem3  9704  cardlim  9887  carduni  9896  alephordi  9987  alephval3  10023  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axcclem  10370  zorn2lem5  10413  zorn2lem6  10414  axdclem2  10433  alephval2  10486  gruen  10726  grur1a  10733  grothomex  10743  nqereu  10843  distrlem5pr  10941  psslinpr  10945  ltaprlem  10958  suplem1pr  10966  lbreu  12097  fleqceilz  13804  caubnd  15312  divconjdvds  16275  algcvga  16539  algfx  16540  gsummatr01lem3  22632  fiinopn  22876  hausnei  23303  hausnei2  23328  cmpsublem  23374  cmpsub  23375  fcfneii  24012  ppiublem1  27179  sltsun2  27795  nb3grprlem1  29463  cusgrsize2inds  29537  wlk1walk  29722  clwlkclwwlklem2  30085  clwwlkf  30132  clwwlknonwwlknonb  30191  vdgn1frgrv2  30381  frgrncvvdeqlem8  30391  frgrncvvdeqlem9  30392  frgrreggt1  30478  frgrregord013  30480  chintcli  31417  h1datomi  31667  strlem3a  32338  hstrlem3a  32346  mdexchi  32421  cvbr4i  32453  mdsymlem4  32492  mdsymlem6  32494  3jaodd  35913  ifscgr  36242  dfttc4lem2  36727  bj-fvimacnv0  37616  exrecfnlem  37709  wepwsolem  43488  rp-fakeimass  43957  ee233  44964  iccpartgt  47899  lighneal  48086  grlictr  48503  ldepspr  48961