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  418  mob  3710  otiunsndisj  5412  sotri2  5991  sotri3  5992  relresfld  6129  limuni3  7569  poxp  7824  soxp  7825  tz7.49  8083  omwordri  8200  odi  8207  omass  8208  oewordri  8220  nndi  8251  nnmass  8252  r1sdom  9205  tz9.12lem3  9220  cardlim  9403  carduni  9412  alephordi  9502  alephval3  9538  domtriomlem  9866  axdc3lem2  9875  axdc3lem4  9877  axcclem  9881  zorn2lem5  9924  zorn2lem6  9925  axdclem2  9944  alephval2  9996  gruen  10236  grur1a  10243  grothomex  10253  nqereu  10353  distrlem5pr  10451  psslinpr  10455  ltaprlem  10468  suplem1pr  10476  lbreu  11593  fleqceilz  13225  caubnd  14720  divconjdvds  15667  algcvga  15925  algfx  15926  gsummatr01lem3  21268  fiinopn  21511  hausnei  21938  hausnei2  21963  cmpsublem  22009  cmpsub  22010  fcfneii  22647  ppiublem1  25780  nb3grprlem1  27164  cusgrsize2inds  27237  wlk1walk  27422  clwlkclwwlklem2  27780  clwwlkf  27828  clwwlknonwwlknonb  27887  vdgn1frgrv2  28077  frgrncvvdeqlem8  28087  frgrncvvdeqlem9  28088  frgrreggt1  28174  frgrregord013  28176  chintcli  29110  h1datomi  29360  strlem3a  30031  hstrlem3a  30039  mdexchi  30114  cvbr4i  30146  mdsymlem4  30185  mdsymlem6  30187  3jaodd  32946  frr3g  33123  ifscgr  33507  bj-fvimacnv0  34570  exrecfnlem  34662  wepwsolem  39649  rp-fakeimass  39885  ee233  40860  iccpartgt  43594  lighneal  43783  ldepspr  44535