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  elabgtOLD  3618  mob  3665  otiunsndisj  5468  sotri2  6086  sotri3  6087  relresfld  6234  limuni3  7799  poxp  8075  soxp  8076  tz7.49  8381  omwordri  8504  odi  8511  omass  8512  oewordri  8525  nndi  8556  nnmass  8557  frr3g  9678  r1sdom  9696  tz9.12lem3  9711  cardlim  9894  carduni  9903  alephordi  9994  alephval3  10030  domtriomlem  10362  axdc3lem2  10371  axdc3lem4  10373  axcclem  10377  zorn2lem5  10420  zorn2lem6  10421  axdclem2  10440  alephval2  10493  gruen  10733  grur1a  10740  grothomex  10750  nqereu  10850  distrlem5pr  10948  psslinpr  10952  ltaprlem  10965  suplem1pr  10973  lbreu  12104  fleqceilz  13811  caubnd  15319  divconjdvds  16282  algcvga  16546  algfx  16547  gsummatr01lem3  22647  fiinopn  22891  hausnei  23318  hausnei2  23343  cmpsublem  23389  cmpsub  23390  fcfneii  24027  ppiublem1  27190  sltsun2  27806  nb3grprlem1  29474  cusgrsize2inds  29547  wlk1walk  29732  clwlkclwwlklem2  30095  clwwlkf  30142  clwwlknonwwlknonb  30201  vdgn1frgrv2  30391  frgrncvvdeqlem8  30401  frgrncvvdeqlem9  30402  frgrreggt1  30488  frgrregord013  30490  chintcli  31427  h1datomi  31677  strlem3a  32348  hstrlem3a  32356  mdexchi  32431  cvbr4i  32463  mdsymlem4  32502  mdsymlem6  32504  3jaodd  35950  ifscgr  36279  dfttc4lem2  36764  bj-fvimacnv0  37653  exrecfnlem  37748  wepwsolem  43494  rp-fakeimass  43963  ee233  44970  iccpartgt  47909  lighneal  48096  grlictr  48513  ldepspr  48971