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  3627  elabgtOLDOLD  3628  mob  3675  otiunsndisj  5468  sotri2  6086  sotri3  6087  relresfld  6234  limuni3  7794  poxp  8070  soxp  8071  tz7.49  8376  omwordri  8499  odi  8506  omass  8507  oewordri  8520  nndi  8551  nnmass  8552  frr3g  9668  r1sdom  9686  tz9.12lem3  9701  cardlim  9884  carduni  9893  alephordi  9984  alephval3  10020  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  axcclem  10367  zorn2lem5  10410  zorn2lem6  10411  axdclem2  10430  alephval2  10483  gruen  10723  grur1a  10730  grothomex  10740  nqereu  10840  distrlem5pr  10938  psslinpr  10942  ltaprlem  10955  suplem1pr  10963  lbreu  12092  fleqceilz  13774  caubnd  15282  divconjdvds  16242  algcvga  16506  algfx  16507  gsummatr01lem3  22601  fiinopn  22845  hausnei  23272  hausnei2  23297  cmpsublem  23343  cmpsub  23344  fcfneii  23981  ppiublem1  27169  sltsun2  27785  nb3grprlem1  29453  cusgrsize2inds  29527  wlk1walk  29712  clwlkclwwlklem2  30075  clwwlkf  30122  clwwlknonwwlknonb  30181  vdgn1frgrv2  30371  frgrncvvdeqlem8  30381  frgrncvvdeqlem9  30382  frgrreggt1  30468  frgrregord013  30470  chintcli  31406  h1datomi  31656  strlem3a  32327  hstrlem3a  32335  mdexchi  32410  cvbr4i  32442  mdsymlem4  32481  mdsymlem6  32483  3jaodd  35909  ifscgr  36238  bj-fvimacnv0  37491  exrecfnlem  37584  wepwsolem  43284  rp-fakeimass  43753  ee233  44760  iccpartgt  47673  lighneal  47857  grlictr  48261  ldepspr  48719