Theorem 3com23 1127

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 1126	. 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
3	2	3com12 1124	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3coml  1128  3anidm13  1422  eqreu  3735  f1ofveu  7425  curry2f  8133  dfsmo2  8387  nneob  8694  nadd32  8735  f1oeng  9011  domnsymfi  9240  sdomdomtrfi  9241  domsdomtrfi  9242  php  9247  php3  9249  fodomfir  9368  suppr  9511  infdif  10248  axdclem2  10560  gchen1  10665  grumap  10848  grudomon  10857  mul32  11427  add32  11480  subsub23  11513  subadd23  11520  addsub12  11521  subsub  11539  subsub3  11541  sub32  11543  suble  11741  lesub  11742  ltsub23  11743  ltsub13  11744  ltleadd  11746  div32  11942  div13  11943  div12  11944  divdiv32  11975  cju  12262  infssuzle  12973  ioo0  13412  ico0  13433  ioc0  13434  icc0  13435  fzen  13581  modcyc  13946  expgt0  14136  expge0  14139  expge1  14140  2cshwcom  14854  shftval2  15114  abs3dif  15370  divalgb  16441  submrc  17671  mrieqv2d  17682  pltnlt  18385  pltn2lp  18386  tosso  18464  latnle  18518  latabs1  18520  lubel  18559  ipopos  18581  grpinvcnv  19024  mulgaddcom  19116  mulgneg2  19126  oppgmnd  19373  oddvdsnn0  19562  oddvds  19565  odmulg  19574  odcl2  19583  lsmcomx  19874  srgcom4  20211  srgrmhm  20219  ringcom  20277  mulgass2  20306  opprrng  20345  irredrmul  20427  irredlmul  20428  isdrngrd  20766  isdrngrdOLD  20768  islmodd  20864  lmodcom  20906  rmodislmod  20928  zntoslem  21575  ipcl  21651  evls1fpws  22373  maducoevalmin1  22658  rintopn  22915  opnnei  23128  restin  23174  cnpnei  23272  cnprest  23297  ordthaus  23392  kgen2ss  23563  hausflim  23989  fclsfnflim  24035  cnpfcf  24049  opnsubg  24116  cuspcvg  24310  psmetsym  24320  xmetsym  24357  ngpdsr  24618  ngpds2r  24620  ngpds3r  24622  clmmulg  25134  cphipval2  25275  iscau2  25311  dgr1term  26299  cxpeq0  26720  cxpge0  26725  relogbzcl  26817  negsunif  28087  grpoidinvlem2  30524  grpoinvdiv  30556  nvpncan  30673  nvabs  30691  ipval2lem2  30723  dipcj  30733  diporthcom  30735  dipdi  30862  dipassr  30865  dipsubdi  30868  hlipcj  30930  hvadd32  31053  hvsub32  31064  his5  31105  hoadd32  31802  hosubsub  31836  unopf1o  31935  adj2  31953  adjvalval  31956  adjlnop  32105  leopmul2i  32154  cvntr  32311  mdsymlem5  32426  sumdmdii  32434  supxrnemnf  32772  odutos  32958  tlt2  32959  tosglblem  32964  archiabl  33205  unitdivcld  33900  bnj605  34921  bnj607  34930  fisshasheq  35120  swrdrevpfx  35122  cusgredgex  35127  acycgr1v  35154  gcd32  35749  cgrrflx  35988  cgrcom  35991  cgrcomr  35998  btwntriv1  36017  cgr3com  36054  colineartriv2  36069  segleantisym  36116  seglelin  36117  btwnoutside  36126  clsint2  36330  dissneqlem  37341  ftc1anclem5  37704  heibor1  37817  rngoidl  38031  ispridlc  38077  opltcon3b  39205  cmtcomlemN  39249  cmtcomN  39250  cmt3N  39252  cmtbr3N  39255  cvrval2  39275  cvrnbtwn4  39280  leatb  39293  atlrelat1  39322  hlatlej2  39377  hlateq  39401  hlrelat5N  39403  snatpsubN  39752  pmap11  39764  paddcom  39815  sspadd2  39818  paddss12  39821  cdleme51finvN  40558  cdleme51finvtrN  40560  cdlemeiota  40587  cdlemg2jlemOLDN  40595  cdlemg2klem  40597  cdlemg4b1  40611  cdlemg4b2  40612  trljco2  40743  tgrpabl  40753  tendoplcom  40784  cdleml6  40983  erngdvlem3-rN  41000  dia11N  41050  dib11N  41162  dih11  41267  uzindd  41978  lcmineqlem1  42030  nerabdioph  42820  monotoddzzfi  42954  fzneg  42994  jm2.19lem2  43002  ismnushort  44320  nzss  44336  sineq0ALT  44957  lincvalsng  48333  reccot  49277