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  3625  elabgtOLDOLD  3626  mob  3673  otiunsndisj  5465  sotri2  6083  sotri3  6084  relresfld  6231  limuni3  7791  poxp  8067  soxp  8068  tz7.49  8373  omwordri  8496  odi  8503  omass  8504  oewordri  8516  nndi  8547  nnmass  8548  frr3g  9659  r1sdom  9677  tz9.12lem3  9692  cardlim  9875  carduni  9884  alephordi  9975  alephval3  10011  domtriomlem  10343  axdc3lem2  10352  axdc3lem4  10354  axcclem  10358  zorn2lem5  10401  zorn2lem6  10402  axdclem2  10421  alephval2  10473  gruen  10713  grur1a  10720  grothomex  10730  nqereu  10830  distrlem5pr  10928  psslinpr  10932  ltaprlem  10945  suplem1pr  10953  lbreu  12082  fleqceilz  13768  caubnd  15276  divconjdvds  16236  algcvga  16500  algfx  16501  gsummatr01lem3  22582  fiinopn  22826  hausnei  23253  hausnei2  23278  cmpsublem  23324  cmpsub  23325  fcfneii  23962  ppiublem1  27150  ssltun2  27760  nb3grprlem1  29369  cusgrsize2inds  29443  wlk1walk  29628  clwlkclwwlklem2  29991  clwwlkf  30038  clwwlknonwwlknonb  30097  vdgn1frgrv2  30287  frgrncvvdeqlem8  30297  frgrncvvdeqlem9  30298  frgrreggt1  30384  frgrregord013  30386  chintcli  31322  h1datomi  31572  strlem3a  32243  hstrlem3a  32251  mdexchi  32326  cvbr4i  32358  mdsymlem4  32397  mdsymlem6  32399  3jaodd  35770  ifscgr  36099  bj-fvimacnv0  37341  exrecfnlem  37434  wepwsolem  43149  rp-fakeimass  43619  ee233  44626  iccpartgt  47541  lighneal  47725  grlictr  48129  ldepspr  48588