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  3630  elabgtOLDOLD  3631  mob  3679  otiunsndisj  5467  sotri2  6082  sotri3  6083  relresfld  6228  limuni3  7792  poxp  8068  soxp  8069  tz7.49  8374  omwordri  8497  odi  8504  omass  8505  oewordri  8517  nndi  8548  nnmass  8549  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  10485  gruen  10725  grur1a  10732  grothomex  10742  nqereu  10842  distrlem5pr  10940  psslinpr  10944  ltaprlem  10957  suplem1pr  10965  lbreu  12093  fleqceilz  13776  caubnd  15284  divconjdvds  16244  algcvga  16508  algfx  16509  gsummatr01lem3  22560  fiinopn  22804  hausnei  23231  hausnei2  23256  cmpsublem  23302  cmpsub  23303  fcfneii  23940  ppiublem1  27129  ssltun2  27738  nb3grprlem1  29343  cusgrsize2inds  29417  wlk1walk  29602  clwlkclwwlklem2  29962  clwwlkf  30009  clwwlknonwwlknonb  30068  vdgn1frgrv2  30258  frgrncvvdeqlem8  30268  frgrncvvdeqlem9  30269  frgrreggt1  30355  frgrregord013  30357  chintcli  31293  h1datomi  31543  strlem3a  32214  hstrlem3a  32222  mdexchi  32297  cvbr4i  32329  mdsymlem4  32368  mdsymlem6  32370  3jaodd  35690  ifscgr  36020  bj-fvimacnv0  37262  exrecfnlem  37355  wepwsolem  43018  rp-fakeimass  43488  ee233  44496  iccpartgt  47415  lighneal  47599  grlictr  48003  ldepspr  48462