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  3628  elabgtOLDOLD  3629  mob  3676  otiunsndisj  5460  sotri2  6076  sotri3  6077  relresfld  6223  limuni3  7782  poxp  8058  soxp  8059  tz7.49  8364  omwordri  8487  odi  8494  omass  8495  oewordri  8507  nndi  8538  nnmass  8539  frr3g  9649  r1sdom  9667  tz9.12lem3  9682  cardlim  9865  carduni  9874  alephordi  9965  alephval3  10001  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  axcclem  10348  zorn2lem5  10391  zorn2lem6  10392  axdclem2  10411  alephval2  10463  gruen  10703  grur1a  10710  grothomex  10720  nqereu  10820  distrlem5pr  10918  psslinpr  10922  ltaprlem  10935  suplem1pr  10943  lbreu  12072  fleqceilz  13758  caubnd  15266  divconjdvds  16226  algcvga  16490  algfx  16491  gsummatr01lem3  22573  fiinopn  22817  hausnei  23244  hausnei2  23269  cmpsublem  23315  cmpsub  23316  fcfneii  23953  ppiublem1  27141  ssltun2  27751  nb3grprlem1  29359  cusgrsize2inds  29433  wlk1walk  29618  clwlkclwwlklem2  29978  clwwlkf  30025  clwwlknonwwlknonb  30084  vdgn1frgrv2  30274  frgrncvvdeqlem8  30284  frgrncvvdeqlem9  30285  frgrreggt1  30371  frgrregord013  30373  chintcli  31309  h1datomi  31559  strlem3a  32230  hstrlem3a  32238  mdexchi  32313  cvbr4i  32345  mdsymlem4  32384  mdsymlem6  32386  3jaodd  35757  ifscgr  36084  bj-fvimacnv0  37326  exrecfnlem  37419  wepwsolem  43081  rp-fakeimass  43551  ee233  44558  iccpartgt  47464  lighneal  47648  grlictr  48052  ldepspr  48511