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  3685  f1ofveu  7350  curry2f  8048  dfsmo2  8277  nneob  8582  nadd32  8623  f1oeng  8905  domnsymfi  9122  sdomdomtrfi  9123  domsdomtrfi  9124  php  9129  php3  9131  fodomfir  9226  suppr  9373  infdif  10116  axdclem2  10428  gchen1  10534  grumap  10717  grudomon  10726  mul32  11297  add32  11350  subsub23  11383  subadd23  11390  addsub12  11391  subsub  11409  subsub3  11411  sub32  11413  suble  11613  lesub  11614  ltsub23  11615  ltsub13  11616  ltleadd  11618  div32  11814  div13  11815  div12  11816  divdiv32  11847  cju  12139  infssuzle  12842  ioo0  13284  ico0  13305  ioc0  13306  icc0  13307  fzen  13455  modcyc  13824  expgt0  14016  expge0  14019  expge1  14020  2cshwcom  14737  shftval2  14996  abs3dif  15253  divalgb  16329  submrc  17549  mrieqv2d  17560  pltnlt  18259  pltn2lp  18260  tosso  18338  latnle  18394  latabs1  18396  lubel  18435  ipopos  18457  grpinvcnv  18934  mulgaddcom  19026  mulgneg2  19036  oppgmnd  19281  oddvdsnn0  19471  oddvds  19474  odmulg  19483  odcl2  19492  lsmcomx  19783  srgcom4  20147  srgrmhm  20155  ringcom  20213  mulgass2  20242  opprrng  20279  irredrmul  20361  irredlmul  20362  isdrngrd  20697  isdrngrdOLD  20699  islmodd  20815  lmodcom  20857  rmodislmod  20879  zntoslem  21509  ipcl  21586  evls1fpws  22311  maducoevalmin1  22594  rintopn  22851  opnnei  23062  restin  23108  cnpnei  23206  cnprest  23231  ordthaus  23326  kgen2ss  23497  hausflim  23923  fclsfnflim  23969  cnpfcf  23983  opnsubg  24050  cuspcvg  24242  psmetsym  24252  xmetsym  24289  ngpdsr  24547  ngpds2r  24549  ngpds3r  24551  clmmulg  25055  cphipval2  25195  iscau2  25231  dgr1term  26219  cxpeq0  26641  cxpge0  26646  relogbzcl  26738  negsunif  28024  oldfib  28335  grpoidinvlem2  30529  grpoinvdiv  30561  nvpncan  30678  nvabs  30696  ipval2lem2  30728  dipcj  30738  diporthcom  30740  dipdi  30867  dipassr  30870  dipsubdi  30873  hlipcj  30935  hvadd32  31058  hvsub32  31069  his5  31110  hoadd32  31807  hosubsub  31841  unopf1o  31940  adj2  31958  adjvalval  31961  adjlnop  32110  leopmul2i  32159  cvntr  32316  mdsymlem5  32431  sumdmdii  32439  supxrnemnf  32797  odutos  32999  tlt2  33000  tosglblem  33005  archiabl  33229  unitdivcld  34007  bnj605  35012  bnj607  35021  rankfilimb  35207  r1filim  35209  fisshasheq  35258  swrdrevpfx  35260  cusgredgex  35265  acycgr1v  35292  gcd32  35892  cgrrflx  36130  cgrcom  36133  cgrcomr  36140  btwntriv1  36159  cgr3com  36196  colineartriv2  36211  segleantisym  36258  seglelin  36259  btwnoutside  36268  clsint2  36472  dissneqlem  37484  ftc1anclem5  37837  heibor1  37950  rngoidl  38164  ispridlc  38210  opltcon3b  39403  cmtcomlemN  39447  cmtcomN  39448  cmt3N  39450  cmtbr3N  39453  cvrval2  39473  cvrnbtwn4  39478  leatb  39491  atlrelat1  39520  hlatlej2  39575  hlateq  39598  hlrelat5N  39600  snatpsubN  39949  pmap11  39961  paddcom  40012  sspadd2  40015  paddss12  40018  cdleme51finvN  40755  cdleme51finvtrN  40757  cdlemeiota  40784  cdlemg2jlemOLDN  40792  cdlemg2klem  40794  cdlemg4b1  40808  cdlemg4b2  40809  trljco2  40940  tgrpabl  40950  tendoplcom  40981  cdleml6  41180  erngdvlem3-rN  41197  dia11N  41247  dib11N  41359  dih11  41464  uzindd  42170  lcmineqlem1  42222  nerabdioph  42993  monotoddzzfi  43126  fzneg  43166  jm2.19lem2  43174  ismnushort  44484  nzss  44500  sineq0ALT  45119  lincvalsng  48604  reccot  49945