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  419  elabgt  3570  mob  3619  otiunsndisj  5388  sotri2  5974  sotri3  5975  relresfld  6119  limuni3  7609  poxp  7873  soxp  7874  tz7.49  8159  omwordri  8278  odi  8285  omass  8286  oewordri  8298  nndi  8329  nnmass  8330  r1sdom  9355  tz9.12lem3  9370  cardlim  9553  carduni  9562  alephordi  9653  alephval3  9689  domtriomlem  10021  axdc3lem2  10030  axdc3lem4  10032  axcclem  10036  zorn2lem5  10079  zorn2lem6  10080  axdclem2  10099  alephval2  10151  gruen  10391  grur1a  10398  grothomex  10408  nqereu  10508  distrlem5pr  10606  psslinpr  10610  ltaprlem  10623  suplem1pr  10631  lbreu  11747  fleqceilz  13392  caubnd  14887  divconjdvds  15839  algcvga  16099  algfx  16100  gsummatr01lem3  21508  fiinopn  21752  hausnei  22179  hausnei2  22204  cmpsublem  22250  cmpsub  22251  fcfneii  22888  ppiublem1  26037  nb3grprlem1  27422  cusgrsize2inds  27495  wlk1walk  27680  clwlkclwwlklem2  28037  clwwlkf  28084  clwwlknonwwlknonb  28143  vdgn1frgrv2  28333  frgrncvvdeqlem8  28343  frgrncvvdeqlem9  28344  frgrreggt1  28430  frgrregord013  28432  chintcli  29366  h1datomi  29616  strlem3a  30287  hstrlem3a  30295  mdexchi  30370  cvbr4i  30402  mdsymlem4  30441  mdsymlem6  30443  3jaodd  33326  frr3g  33504  ssltun2  33689  ifscgr  34032  bj-fvimacnv0  35141  exrecfnlem  35236  wepwsolem  40511  rp-fakeimass  40745  ee233  41753  iccpartgt  44495  lighneal  44679  ldepspr  45430