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  416  elabgt  3604  mob  3653  otiunsndisj  5435  sotri2  6039  sotri3  6040  relresfld  6183  limuni3  7708  poxp  7978  soxp  7979  tz7.49  8285  omwordri  8412  odi  8419  omass  8420  oewordri  8432  nndi  8463  nnmass  8464  frr3g  9523  r1sdom  9541  tz9.12lem3  9556  cardlim  9739  carduni  9748  alephordi  9839  alephval3  9875  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  axcclem  10222  zorn2lem5  10265  zorn2lem6  10266  axdclem2  10285  alephval2  10337  gruen  10577  grur1a  10584  grothomex  10594  nqereu  10694  distrlem5pr  10792  psslinpr  10796  ltaprlem  10809  suplem1pr  10817  lbreu  11934  fleqceilz  13583  caubnd  15079  divconjdvds  16033  algcvga  16293  algfx  16294  gsummatr01lem3  21815  fiinopn  22059  hausnei  22488  hausnei2  22513  cmpsublem  22559  cmpsub  22560  fcfneii  23197  ppiublem1  26359  nb3grprlem1  27756  cusgrsize2inds  27829  wlk1walk  28015  clwlkclwwlklem2  28373  clwwlkf  28420  clwwlknonwwlknonb  28479  vdgn1frgrv2  28669  frgrncvvdeqlem8  28679  frgrncvvdeqlem9  28680  frgrreggt1  28766  frgrregord013  28768  chintcli  29702  h1datomi  29952  strlem3a  30623  hstrlem3a  30631  mdexchi  30706  cvbr4i  30738  mdsymlem4  30777  mdsymlem6  30779  3jaodd  33666  ssltun2  34012  ifscgr  34355  bj-fvimacnv0  35466  exrecfnlem  35559  wepwsolem  40874  rp-fakeimass  41126  ee233  42146  iccpartgt  44890  lighneal  45074  ldepspr  45825