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  elabgt  3596  mob  3647  otiunsndisj  5428  sotri2  6023  sotri3  6024  relresfld  6168  limuni3  7674  poxp  7940  soxp  7941  tz7.49  8246  omwordri  8365  odi  8372  omass  8373  oewordri  8385  nndi  8416  nnmass  8417  frr3g  9445  r1sdom  9463  tz9.12lem3  9478  cardlim  9661  carduni  9670  alephordi  9761  alephval3  9797  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axcclem  10144  zorn2lem5  10187  zorn2lem6  10188  axdclem2  10207  alephval2  10259  gruen  10499  grur1a  10506  grothomex  10516  nqereu  10616  distrlem5pr  10714  psslinpr  10718  ltaprlem  10731  suplem1pr  10739  lbreu  11855  fleqceilz  13502  caubnd  14998  divconjdvds  15952  algcvga  16212  algfx  16213  gsummatr01lem3  21714  fiinopn  21958  hausnei  22387  hausnei2  22412  cmpsublem  22458  cmpsub  22459  fcfneii  23096  ppiublem1  26255  nb3grprlem1  27650  cusgrsize2inds  27723  wlk1walk  27908  clwlkclwwlklem2  28265  clwwlkf  28312  clwwlknonwwlknonb  28371  vdgn1frgrv2  28561  frgrncvvdeqlem8  28571  frgrncvvdeqlem9  28572  frgrreggt1  28658  frgrregord013  28660  chintcli  29594  h1datomi  29844  strlem3a  30515  hstrlem3a  30523  mdexchi  30598  cvbr4i  30630  mdsymlem4  30669  mdsymlem6  30671  3jaodd  33559  ssltun2  33930  ifscgr  34273  bj-fvimacnv0  35384  exrecfnlem  35477  wepwsolem  40783  rp-fakeimass  41017  ee233  42028  iccpartgt  44767  lighneal  44951  ldepspr  45702