Theorem 3com23 1126

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

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3comr 1125	. 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
3	2	3com12 1123	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3coml  1127  3anidm13  1422  eqreu  3703  f1ofveu  7384  curry2f  8090  dfsmo2  8319  nneob  8623  nadd32  8664  f1oeng  8945  domnsymfi  9170  sdomdomtrfi  9171  domsdomtrfi  9172  php  9177  php3  9179  fodomfir  9286  suppr  9430  infdif  10168  axdclem2  10480  gchen1  10585  grumap  10768  grudomon  10777  mul32  11347  add32  11400  subsub23  11433  subadd23  11440  addsub12  11441  subsub  11459  subsub3  11461  sub32  11463  suble  11663  lesub  11664  ltsub23  11665  ltsub13  11666  ltleadd  11668  div32  11864  div13  11865  div12  11866  divdiv32  11897  cju  12189  infssuzle  12897  ioo0  13338  ico0  13359  ioc0  13360  icc0  13361  fzen  13509  modcyc  13875  expgt0  14067  expge0  14070  expge1  14071  2cshwcom  14788  shftval2  15048  abs3dif  15305  divalgb  16381  submrc  17596  mrieqv2d  17607  pltnlt  18306  pltn2lp  18307  tosso  18385  latnle  18439  latabs1  18441  lubel  18480  ipopos  18502  grpinvcnv  18945  mulgaddcom  19037  mulgneg2  19047  oppgmnd  19293  oddvdsnn0  19481  oddvds  19484  odmulg  19493  odcl2  19502  lsmcomx  19793  srgcom4  20130  srgrmhm  20138  ringcom  20196  mulgass2  20225  opprrng  20261  irredrmul  20343  irredlmul  20344  isdrngrd  20682  isdrngrdOLD  20684  islmodd  20779  lmodcom  20821  rmodislmod  20843  zntoslem  21473  ipcl  21549  evls1fpws  22263  maducoevalmin1  22546  rintopn  22803  opnnei  23014  restin  23060  cnpnei  23158  cnprest  23183  ordthaus  23278  kgen2ss  23449  hausflim  23875  fclsfnflim  23921  cnpfcf  23935  opnsubg  24002  cuspcvg  24195  psmetsym  24205  xmetsym  24242  ngpdsr  24500  ngpds2r  24502  ngpds3r  24504  clmmulg  25008  cphipval2  25148  iscau2  25184  dgr1term  26172  cxpeq0  26594  cxpge0  26599  relogbzcl  26691  negsunif  27968  grpoidinvlem2  30441  grpoinvdiv  30473  nvpncan  30590  nvabs  30608  ipval2lem2  30640  dipcj  30650  diporthcom  30652  dipdi  30779  dipassr  30782  dipsubdi  30785  hlipcj  30847  hvadd32  30970  hvsub32  30981  his5  31022  hoadd32  31719  hosubsub  31753  unopf1o  31852  adj2  31870  adjvalval  31873  adjlnop  32022  leopmul2i  32071  cvntr  32228  mdsymlem5  32343  sumdmdii  32351  supxrnemnf  32698  odutos  32901  tlt2  32902  tosglblem  32907  archiabl  33159  unitdivcld  33898  bnj605  34904  bnj607  34913  fisshasheq  35109  swrdrevpfx  35111  cusgredgex  35116  acycgr1v  35143  gcd32  35743  cgrrflx  35982  cgrcom  35985  cgrcomr  35992  btwntriv1  36011  cgr3com  36048  colineartriv2  36063  segleantisym  36110  seglelin  36111  btwnoutside  36120  clsint2  36324  dissneqlem  37335  ftc1anclem5  37698  heibor1  37811  rngoidl  38025  ispridlc  38071  opltcon3b  39204  cmtcomlemN  39248  cmtcomN  39249  cmt3N  39251  cmtbr3N  39254  cvrval2  39274  cvrnbtwn4  39279  leatb  39292  atlrelat1  39321  hlatlej2  39376  hlateq  39400  hlrelat5N  39402  snatpsubN  39751  pmap11  39763  paddcom  39814  sspadd2  39817  paddss12  39820  cdleme51finvN  40557  cdleme51finvtrN  40559  cdlemeiota  40586  cdlemg2jlemOLDN  40594  cdlemg2klem  40596  cdlemg4b1  40610  cdlemg4b2  40611  trljco2  40742  tgrpabl  40752  tendoplcom  40783  cdleml6  40982  erngdvlem3-rN  40999  dia11N  41049  dib11N  41161  dih11  41266  uzindd  41972  lcmineqlem1  42024  nerabdioph  42804  monotoddzzfi  42938  fzneg  42978  jm2.19lem2  42986  ismnushort  44297  nzss  44313  sineq0ALT  44933  lincvalsng  48409  reccot  49751