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

Theorem 3com23 1269
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 1262 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1254 1 ((𝜑𝜒𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  3coml  1270  syld3an2  1371  3anidm13  1382  eqreu  3392  f1ofveu  6630  curry2f  7258  dfsmo2  7429  nneob  7717  f1oeng  7959  suppr  8362  infdif  9016  axdclem2  9327  gchen1  9432  grumap  9615  grudomon  9624  mul32  10188  add32  10239  subsub23  10271  subadd23  10278  addsub12  10279  subsub  10296  subsub3  10298  sub32  10300  suble  10491  lesub  10492  ltsub23  10493  ltsub13  10494  ltleadd  10496  div32  10690  div13  10691  div12  10692  divdiv32  10718  cju  11001  infssuzle  11756  ioo0  12185  ico0  12206  ioc0  12207  icc0  12208  fzen  12343  elfz1b  12394  modcyc  12688  expgt0  12876  expge0  12879  expge1  12880  2cshwcom  13543  shftval2  13796  abs3dif  14052  divalgb  15108  submrc  16269  mrieqv2d  16280  pltnlt  16949  pltn2lp  16950  tosso  17017  latnle  17066  latabs1  17068  lubel  17103  ipopos  17141  grpinvcnv  17464  mulgneg2  17556  oppgmnd  17765  oddvdsnn0  17944  oddvds  17947  odmulg  17954  odcl2  17963  lsmcomx  18240  srgrmhm  18517  ringcom  18560  mulgass2  18582  opprring  18612  irredrmul  18688  irredlmul  18689  isdrngrd  18754  islmodd  18850  lmodcom  18890  rmodislmod  18912  opprdomn  19282  zntoslem  19886  ipcl  19959  maducoevalmin1  20439  rintopn  20695  opnnei  20905  restin  20951  cnpnei  21049  cnprest  21074  ordthaus  21169  kgen2ss  21339  hausflim  21766  fclsfnflim  21812  cnpfcf  21826  opnsubg  21892  cuspcvg  22086  psmetsym  22096  xmetsym  22133  ngpdsr  22390  ngpds2r  22392  ngpds3r  22394  clmmulg  22882  cphipval2  23021  iscau2  23056  dgr1term  23997  cxpeq0  24405  cxpge0  24410  relogbzcl  24493  grpoidinvlem2  27329  grpoinvdiv  27361  nvpncan  27479  nvabs  27497  ipval2lem2  27529  dipcj  27539  diporthcom  27541  dipdi  27668  dipassr  27671  dipsubdi  27674  hlipcj  27737  hvadd32  27861  hvsub32  27872  his5  27913  hoadd32  28612  hosubsub  28646  unopf1o  28745  adj2  28763  adjvalval  28766  adjlnop  28915  leopmul2i  28964  cvntr  29121  mdsymlem5  29236  sumdmdii  29244  supxrnemnf  29508  odutos  29637  tlt2  29638  tosglblem  29643  archiabl  29726  unitdivcld  29921  bnj605  30951  bnj607  30960  gcd32  31612  cgrrflx  32069  cgrcom  32072  cgrcomr  32079  btwntriv1  32098  cgr3com  32135  colineartriv2  32150  segleantisym  32197  seglelin  32198  btwnoutside  32207  clsint2  32299  dissneqlem  33158  ftc1anclem5  33460  heibor1  33580  rngoidl  33794  ispridlc  33840  opltcon3b  34310  cmtcomlemN  34354  cmtcomN  34355  cmt3N  34357  cmtbr3N  34360  cvrval2  34380  cvrnbtwn4  34385  leatb  34398  atlrelat1  34427  hlatlej2  34481  hlateq  34504  hlrelat5N  34506  snatpsubN  34855  pmap11  34867  paddcom  34918  sspadd2  34921  paddss12  34924  cdleme51finvN  35663  cdleme51finvtrN  35665  cdlemeiota  35692  cdlemg2jlemOLDN  35700  cdlemg2klem  35702  cdlemg4b1  35716  cdlemg4b2  35717  trljco2  35848  tgrpabl  35858  tendoplcom  35889  cdleml6  36088  erngdvlem3-rN  36105  dia11N  36156  dib11N  36268  dih11  36373  nerabdioph  37192  monotoddzzfi  37326  fzneg  37368  jm2.19lem2  37376  nzss  38336  sineq0ALT  38993  lincvalsng  41970  reccot  42264
  Copyright terms: Public domain W3C validator