MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com3r Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
32com12 32 1 (𝜒 → (𝜑 → (𝜓𝜃)))
Colors of variables: wff setvar class
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  mob  3649  otiunsndisj  5308  sotri2  5872  sotri3  5873  relresfld  6009  limuni3  7430  poxp  7682  soxp  7683  tz7.49  7939  omwordri  8055  odi  8062  omass  8063  oewordri  8075  nndi  8106  nnmass  8107  r1sdom  9056  tz9.12lem3  9071  cardlim  9254  carduni  9263  alephordi  9353  alephval3  9389  domtriomlem  9717  axdc3lem2  9726  axdc3lem4  9728  axcclem  9732  zorn2lem5  9775  zorn2lem6  9776  axdclem2  9795  alephval2  9847  gruen  10087  grur1a  10094  grothomex  10104  nqereu  10204  distrlem5pr  10302  psslinpr  10306  ltaprlem  10319  suplem1pr  10327  lbreu  11445  fleqceilz  13076  caubnd  14556  divconjdvds  15502  algcvga  15756  algfx  15757  gsummatr01lem3  20954  fiinopn  21197  hausnei  21624  hausnei2  21649  cmpsublem  21695  cmpsub  21696  fcfneii  22333  ppiublem1  25464  nb3grprlem1  26849  cusgrsize2inds  26922  wlk1walk  27107  clwlkclwwlklem2  27464  clwwlkf  27512  vdgn1frgrv2  27763  frgrncvvdeqlem8  27773  frgrncvvdeqlem9  27774  frgrreggt1  27860  frgrregord013  27862  chintcli  28795  h1datomi  29045  strlem3a  29716  hstrlem3a  29724  mdexchi  29799  cvbr4i  29831  mdsymlem4  29870  mdsymlem6  29872  3jaodd  32554  frr3g  32732  ifscgr  33116  exrecfnlem  34212  wepwsolem  39148  rp-fakeimass  39384  ee233  40413  iccpartgt  43091  lighneal  43280  ldepspr  44030
  Copyright terms: Public domain W3C validator