Theorem com3r 88

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 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
3	2	com12 33	1 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com13  89  com3l  90  com14  97  expd  421  elabgtOLD  3630  mob  3678  otiunsndisj  5498  sotri2  6136  sotri3  6137  relresfldOLD  6298  limuni3  7890  poxp  8170  soxp  8171  tz7.49  8486  omwordri  8611  odi  8618  omass  8619  oewordri  8632  nndi  8663  nnmass  8664  frr3g  9790  r1sdom  9811  tz9.12lem3  9826  cardlim  10083  carduni  10092  alephordi  10183  alephval3  10219  domtriomlem  10550  axdc3lem2  10559  axdc3lem4  10561  axcclem  10565  zorn2lem5  10608  zorn2lem6  10609  axdclem2  10628  alephval2  10687  gruen  10927  grur1a  10934  grothomex  10944  nqereu  11044  distrlem5pr  11142  psslinpr  11146  ltaprlem  11159  suplem1pr  11167  lbreu  12297  fleqceilz  14024  caubnd  15558  divconjdvds  16517  algcvga  16786  algfx  16787  gsummatr01lem3  23005  fiinopn  23252  hausnei  23679  hausnei2  23704  cmpsublem  23750  cmpsub  23751  fcfneii  24389  ppiublem1  27562  sltsun2  28208  nb3grprlem1  29994  cusgrsize2inds  30067  wlk1walk  30252  clwlkclwwlklem2  30624  clwwlkf  30671  clwwlknonwwlknonb  30730  vdgn1frgrv2  30930  frgrncvvdeqlem8  30940  frgrncvvdeqlem9  30941  frgrreggt1  31027  frgrregord013  31029  chintcli  31966  h1datomi  32216  strlem3a  32887  hstrlem3a  32895  mdexchi  32970  cvbr4i  33002  mdsymlem4  33041  mdsymlem6  33043  3jaodd  36671  ifscgr  37000  dfttc4lem2  37508  bj-fvimacnv0  38412  exrecfnlem  38507  wepwsolem  44253  rp-fakeimass  44716  ee233  45704  iccpartgt  48724  lighneal  48911  grlictr  49328  ldepspr  49800