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

Theorem 3com23 1118
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 1117 . 2 ((𝜒𝜑𝜓) → 𝜃)
323com12 1115 1 ((𝜑𝜒𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3coml  1119  3anidm13  1412  eqreu  3719  f1ofveu  7140  curry2f  7794  dfsmo2  7975  nneob  8269  f1oeng  8517  suppr  8924  infdif  9620  axdclem2  9931  gchen1  10036  grumap  10219  grudomon  10228  mul32  10795  add32  10847  subsub23  10880  subadd23  10887  addsub12  10888  subsub  10905  subsub3  10907  sub32  10909  suble  11107  lesub  11108  ltsub23  11109  ltsub13  11110  ltleadd  11112  div32  11307  div13  11308  div12  11309  divdiv32  11337  cju  11623  infssuzle  12320  ioo0  12753  ico0  12774  ioc0  12775  icc0  12776  fzen  12914  modcyc  13264  expgt0  13452  expge0  13455  expge1  13456  2cshwcom  14168  shftval2  14424  abs3dif  14681  divalgb  15745  submrc  16889  mrieqv2d  16900  pltnlt  17568  pltn2lp  17569  tosso  17636  latnle  17685  latabs1  17687  lubel  17722  ipopos  17760  grpinvcnv  18107  mulgaddcom  18191  mulgneg2  18201  oppgmnd  18422  oddvdsnn0  18603  oddvds  18606  odmulg  18614  odcl2  18623  lsmcomx  18907  srgrmhm  19217  ringcom  19260  mulgass2  19282  opprring  19312  irredrmul  19388  irredlmul  19389  isdrngrd  19459  islmodd  19571  lmodcom  19611  rmodislmod  19633  opprdomn  20004  zntoslem  20633  ipcl  20707  maducoevalmin1  21191  rintopn  21447  opnnei  21658  restin  21704  cnpnei  21802  cnprest  21827  ordthaus  21922  kgen2ss  22093  hausflim  22519  fclsfnflim  22565  cnpfcf  22579  opnsubg  22645  cuspcvg  22839  psmetsym  22849  xmetsym  22886  ngpdsr  23143  ngpds2r  23145  ngpds3r  23147  clmmulg  23634  cphipval2  23773  iscau2  23809  dgr1term  24779  cxpeq0  25188  cxpge0  25193  relogbzcl  25279  grpoidinvlem2  28210  grpoinvdiv  28242  nvpncan  28359  nvabs  28377  ipval2lem2  28409  dipcj  28419  diporthcom  28421  dipdi  28548  dipassr  28551  dipsubdi  28554  hlipcj  28616  hvadd32  28739  hvsub32  28750  his5  28791  hoadd32  29488  hosubsub  29522  unopf1o  29621  adj2  29639  adjvalval  29642  adjlnop  29791  leopmul2i  29840  cvntr  29997  mdsymlem5  30112  sumdmdii  30120  supxrnemnf  30420  odutos  30578  tlt2  30579  tosglblem  30584  archiabl  30755  unitdivcld  31044  bnj605  32079  bnj607  32088  fisshasheq  32250  swrdrevpfx  32261  cusgredgex  32266  acycgr1v  32294  gcd32  32881  cgrrflx  33346  cgrcom  33349  cgrcomr  33356  btwntriv1  33375  cgr3com  33412  colineartriv2  33427  segleantisym  33474  seglelin  33475  btwnoutside  33484  clsint2  33575  dissneqlem  34504  ftc1anclem5  34853  heibor1  34971  rngoidl  35185  ispridlc  35231  opltcon3b  36222  cmtcomlemN  36266  cmtcomN  36267  cmt3N  36269  cmtbr3N  36272  cvrval2  36292  cvrnbtwn4  36297  leatb  36310  atlrelat1  36339  hlatlej2  36394  hlateq  36417  hlrelat5N  36419  snatpsubN  36768  pmap11  36780  paddcom  36831  sspadd2  36834  paddss12  36837  cdleme51finvN  37574  cdleme51finvtrN  37576  cdlemeiota  37603  cdlemg2jlemOLDN  37611  cdlemg2klem  37613  cdlemg4b1  37627  cdlemg4b2  37628  trljco2  37759  tgrpabl  37769  tendoplcom  37800  cdleml6  37999  erngdvlem3-rN  38016  dia11N  38066  dib11N  38178  dih11  38283  nerabdioph  39286  monotoddzzfi  39419  fzneg  39459  jm2.19lem2  39467  nzss  40529  sineq0ALT  41151  lincvalsng  44369  reccot  44755
  Copyright terms: Public domain W3C validator