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

Theorem 3com23 1262
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com23 ((𝜑𝜒𝜓) → 𝜃)

Proof of Theorem 3com23
StepHypRef Expression
1 3exp.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213exp 1255 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 83 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1248 1 ((𝜑𝜒𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3coml  1263  syld3an2  1364  3anidm13  1375  eqreu  3361  f1ofveu  6519  curry2f  7134  dfsmo2  7305  nneob  7593  f1oeng  7834  suppr  8234  infdif  8888  axdclem2  9199  gchen1  9300  grumap  9483  grudomon  9492  mul32  10051  add32  10102  subsub23  10134  subadd23  10141  addsub12  10142  subsub  10159  subsub3  10161  sub32  10163  suble  10352  lesub  10353  ltsub23  10354  ltsub13  10355  ltleadd  10357  div32  10551  div13  10552  div12  10553  divdiv32  10579  cju  10860  infssuzle  11600  ioo0  12024  ico0  12045  ioc0  12046  icc0  12047  fzen  12181  elfz1b  12231  modcyc  12519  expgt0  12707  expge0  12710  expge1  12711  2cshwcom  13356  shftval2  13606  abs3dif  13862  divalgb  14908  submrc  16054  mrieqv2d  16065  pltnlt  16734  pltn2lp  16735  tosso  16802  latnle  16851  latabs1  16853  lubel  16888  ipopos  16926  grpinvcnv  17249  mulgneg2  17341  oppgmnd  17550  oddvdsnn0  17729  oddvds  17732  odmulg  17739  odcl2  17748  lsmcomx  18025  srgrmhm  18302  ringcom  18345  mulgass2  18367  opprring  18397  irredrmul  18473  irredlmul  18474  isdrngrd  18539  islmodd  18635  lmodcom  18675  opprdomn  19065  zntoslem  19666  ipcl  19739  maducoevalmin1  20216  rintopn  20478  opnnei  20673  restin  20719  cnpnei  20817  cnprest  20842  ordthaus  20937  kgen2ss  21107  hausflim  21534  fclsfnflim  21580  cnpfcf  21594  opnsubg  21660  cuspcvg  21854  psmetsym  21864  xmetsym  21900  ngpdsr  22156  ngpds2r  22158  ngpds3r  22160  clmmulg  22637  iscau2  22798  dgr1term  23734  cxpeq0  24138  cxpge0  24143  relogbzcl  24226  grpoidinvlem2  26506  grpoinvdiv  26538  nvpncan  26679  nvsub  26697  nvabs  26703  nvelbl  26726  ipval2lem2  26741  ipval2lem5  26747  dipcj  26754  diporthcom  26756  dipdi  26885  dipassr  26888  dipsubdi  26891  hlipcj  26954  hvadd32  27078  hvsub32  27089  his5  27130  hoadd32  27829  hosubsub  27863  unopf1o  27962  adj2  27980  adjvalval  27983  adjlnop  28132  leopmul2i  28181  cvntr  28338  mdsymlem5  28453  sumdmdii  28461  supxrnemnf  28727  odutos  28797  tlt2  28798  tosglblem  28803  archiabl  28886  unitdivcld  29078  bnj605  30034  bnj607  30043  gcd32  30693  cgrrflx  31067  cgrcom  31070  cgrcomr  31077  btwntriv1  31096  cgr3com  31133  colineartriv2  31148  segleantisym  31195  seglelin  31196  btwnoutside  31205  clsint2  31297  dissneqlem  32163  ftc1anclem5  32459  heibor1  32579  rngoidl  32793  ispridlc  32839  opltcon3b  33309  cmtcomlemN  33353  cmtcomN  33354  cmt3N  33356  cmtbr3N  33359  cvrval2  33379  cvrnbtwn4  33384  leatb  33397  atlrelat1  33426  hlatlej2  33480  hlateq  33503  hlrelat5N  33505  snatpsubN  33854  pmap11  33866  paddcom  33917  sspadd2  33920  paddss12  33923  cdleme51finvN  34662  cdleme51finvtrN  34664  cdlemeiota  34691  cdlemg2jlemOLDN  34699  cdlemg2klem  34701  cdlemg4b1  34715  cdlemg4b2  34716  trljco2  34847  tgrpabl  34857  tendoplcom  34888  cdleml6  35087  erngdvlem3-rN  35104  dia11N  35155  dib11N  35267  dih11  35372  nerabdioph  36191  monotoddzzfi  36325  fzneg  36367  jm2.19lem2  36375  nzss  37338  sineq0ALT  37995  lincvalsng  41998  reccot  42258
  Copyright terms: Public domain W3C validator