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

Theorem 3com23 1123
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com23 ((𝜑𝜒𝜓) → 𝜃)

Proof of Theorem 3com23
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213comr 1122 . 2 ((𝜒𝜑𝜓) → 𝜃)
323com12 1120 1 ((𝜑𝜒𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086
This theorem is referenced by:  3coml  1124  3anidm13  1417  eqreu  3705  f1ofveu  7133  curry2f  7786  dfsmo2  7967  nneob  8262  f1oeng  8511  suppr  8919  infdif  9616  axdclem2  9927  gchen1  10032  grumap  10215  grudomon  10224  mul32  10791  add32  10843  subsub23  10876  subadd23  10883  addsub12  10884  subsub  10901  subsub3  10903  sub32  10905  suble  11103  lesub  11104  ltsub23  11105  ltsub13  11106  ltleadd  11108  div32  11303  div13  11304  div12  11305  divdiv32  11333  cju  11619  infssuzle  12317  ioo0  12749  ico0  12770  ioc0  12771  icc0  12772  fzen  12917  modcyc  13267  expgt0  13456  expge0  13459  expge1  13460  2cshwcom  14167  shftval2  14423  abs3dif  14680  divalgb  15742  submrc  16888  mrieqv2d  16899  pltnlt  17567  pltn2lp  17568  tosso  17635  latnle  17684  latabs1  17686  lubel  17721  ipopos  17759  grpinvcnv  18156  mulgaddcom  18240  mulgneg2  18250  oppgmnd  18471  oddvdsnn0  18661  oddvds  18664  odmulg  18672  odcl2  18681  lsmcomx  18965  srgrmhm  19275  ringcom  19318  mulgass2  19340  opprring  19370  irredrmul  19446  irredlmul  19447  isdrngrd  19514  islmodd  19626  lmodcom  19666  rmodislmod  19688  opprdomn  20060  zntoslem  20689  ipcl  20763  maducoevalmin1  21247  rintopn  21503  opnnei  21714  restin  21760  cnpnei  21858  cnprest  21883  ordthaus  21978  kgen2ss  22149  hausflim  22575  fclsfnflim  22621  cnpfcf  22635  opnsubg  22702  cuspcvg  22896  psmetsym  22906  xmetsym  22943  ngpdsr  23200  ngpds2r  23202  ngpds3r  23204  clmmulg  23695  cphipval2  23834  iscau2  23870  dgr1term  24846  cxpeq0  25258  cxpge0  25263  relogbzcl  25349  grpoidinvlem2  28277  grpoinvdiv  28309  nvpncan  28426  nvabs  28444  ipval2lem2  28476  dipcj  28486  diporthcom  28488  dipdi  28615  dipassr  28618  dipsubdi  28621  hlipcj  28683  hvadd32  28806  hvsub32  28817  his5  28858  hoadd32  29555  hosubsub  29589  unopf1o  29688  adj2  29706  adjvalval  29709  adjlnop  29858  leopmul2i  29907  cvntr  30064  mdsymlem5  30179  sumdmdii  30187  supxrnemnf  30490  odutos  30647  tlt2  30648  tosglblem  30653  archiabl  30845  unitdivcld  31162  bnj605  32197  bnj607  32206  fisshasheq  32370  swrdrevpfx  32381  cusgredgex  32386  acycgr1v  32414  gcd32  33001  cgrrflx  33466  cgrcom  33469  cgrcomr  33476  btwntriv1  33495  cgr3com  33532  colineartriv2  33547  segleantisym  33594  seglelin  33595  btwnoutside  33604  clsint2  33695  dissneqlem  34659  ftc1anclem5  35034  heibor1  35148  rngoidl  35362  ispridlc  35408  opltcon3b  36400  cmtcomlemN  36444  cmtcomN  36445  cmt3N  36447  cmtbr3N  36450  cvrval2  36470  cvrnbtwn4  36475  leatb  36488  atlrelat1  36517  hlatlej2  36572  hlateq  36595  hlrelat5N  36597  snatpsubN  36946  pmap11  36958  paddcom  37009  sspadd2  37012  paddss12  37015  cdleme51finvN  37752  cdleme51finvtrN  37754  cdlemeiota  37781  cdlemg2jlemOLDN  37789  cdlemg2klem  37791  cdlemg4b1  37805  cdlemg4b2  37806  trljco2  37937  tgrpabl  37947  tendoplcom  37978  cdleml6  38177  erngdvlem3-rN  38194  dia11N  38244  dib11N  38356  dih11  38461  lcmineqlem1  39213  nerabdioph  39582  monotoddzzfi  39715  fzneg  39755  jm2.19lem2  39763  nzss  40857  sineq0ALT  41479  lincvalsng  44666  reccot  45114
  Copyright terms: Public domain W3C validator