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  3642  elabgtOLDOLD  3643  mob  3691  otiunsndisj  5483  sotri2  6105  sotri3  6106  relresfld  6252  limuni3  7831  poxp  8110  soxp  8111  tz7.49  8416  omwordri  8539  odi  8546  omass  8547  oewordri  8559  nndi  8590  nnmass  8591  frr3g  9716  r1sdom  9734  tz9.12lem3  9749  cardlim  9932  carduni  9941  alephordi  10034  alephval3  10070  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axcclem  10417  zorn2lem5  10460  zorn2lem6  10461  axdclem2  10480  alephval2  10532  gruen  10772  grur1a  10779  grothomex  10789  nqereu  10889  distrlem5pr  10987  psslinpr  10991  ltaprlem  11004  suplem1pr  11012  lbreu  12140  fleqceilz  13823  caubnd  15332  divconjdvds  16292  algcvga  16556  algfx  16557  gsummatr01lem3  22551  fiinopn  22795  hausnei  23222  hausnei2  23247  cmpsublem  23293  cmpsub  23294  fcfneii  23931  ppiublem1  27120  ssltun2  27728  nb3grprlem1  29314  cusgrsize2inds  29388  wlk1walk  29574  clwlkclwwlklem2  29936  clwwlkf  29983  clwwlknonwwlknonb  30042  vdgn1frgrv2  30232  frgrncvvdeqlem8  30242  frgrncvvdeqlem9  30243  frgrreggt1  30329  frgrregord013  30331  chintcli  31267  h1datomi  31517  strlem3a  32188  hstrlem3a  32196  mdexchi  32271  cvbr4i  32303  mdsymlem4  32342  mdsymlem6  32344  3jaodd  35709  ifscgr  36039  bj-fvimacnv0  37281  exrecfnlem  37374  wepwsolem  43038  rp-fakeimass  43508  ee233  44516  iccpartgt  47432  lighneal  47616  grlictr  48011  ldepspr  48466