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  417  elabgt  3625  mob  3676  otiunsndisj  5478  sotri2  6084  sotri3  6085  relresfld  6229  limuni3  7789  poxp  8061  soxp  8062  tz7.49  8392  omwordri  8520  odi  8527  omass  8528  oewordri  8540  nndi  8571  nnmass  8572  frr3g  9697  r1sdom  9715  tz9.12lem3  9730  cardlim  9913  carduni  9922  alephordi  10015  alephval3  10051  domtriomlem  10383  axdc3lem2  10392  axdc3lem4  10394  axcclem  10398  zorn2lem5  10441  zorn2lem6  10442  axdclem2  10461  alephval2  10513  gruen  10753  grur1a  10760  grothomex  10770  nqereu  10870  distrlem5pr  10968  psslinpr  10972  ltaprlem  10985  suplem1pr  10993  lbreu  12110  fleqceilz  13765  caubnd  15249  divconjdvds  16202  algcvga  16460  algfx  16461  gsummatr01lem3  22022  fiinopn  22266  hausnei  22695  hausnei2  22720  cmpsublem  22766  cmpsub  22767  fcfneii  23404  ppiublem1  26566  ssltun2  27170  nb3grprlem1  28370  cusgrsize2inds  28443  wlk1walk  28629  clwlkclwwlklem2  28986  clwwlkf  29033  clwwlknonwwlknonb  29092  vdgn1frgrv2  29282  frgrncvvdeqlem8  29292  frgrncvvdeqlem9  29293  frgrreggt1  29379  frgrregord013  29381  chintcli  30315  h1datomi  30565  strlem3a  31236  hstrlem3a  31244  mdexchi  31319  cvbr4i  31351  mdsymlem4  31390  mdsymlem6  31392  3jaodd  34343  ifscgr  34675  bj-fvimacnv0  35803  exrecfnlem  35896  wepwsolem  41412  rp-fakeimass  41872  ee233  42889  iccpartgt  45705  lighneal  45889  ldepspr  46640
  Copyright terms: Public domain W3C validator