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  3712  f1ofveu  7399  curry2f  8107  dfsmo2  8361  nneob  8668  nadd32  8709  f1oeng  8985  domnsymfi  9214  sdomdomtrfi  9215  domsdomtrfi  9216  php  9221  php3  9223  fodomfir  9340  suppr  9484  infdif  10222  axdclem2  10534  gchen1  10639  grumap  10822  grudomon  10831  mul32  11401  add32  11454  subsub23  11487  subadd23  11494  addsub12  11495  subsub  11513  subsub3  11515  sub32  11517  suble  11715  lesub  11716  ltsub23  11717  ltsub13  11718  ltleadd  11720  div32  11916  div13  11917  div12  11918  divdiv32  11949  cju  12236  infssuzle  12947  ioo0  13387  ico0  13408  ioc0  13409  icc0  13410  fzen  13558  modcyc  13923  expgt0  14113  expge0  14116  expge1  14117  2cshwcom  14834  shftval2  15094  abs3dif  15350  divalgb  16423  submrc  17640  mrieqv2d  17651  pltnlt  18350  pltn2lp  18351  tosso  18429  latnle  18483  latabs1  18485  lubel  18524  ipopos  18546  grpinvcnv  18989  mulgaddcom  19081  mulgneg2  19091  oppgmnd  19337  oddvdsnn0  19525  oddvds  19528  odmulg  19537  odcl2  19546  lsmcomx  19837  srgcom4  20174  srgrmhm  20182  ringcom  20240  mulgass2  20269  opprrng  20305  irredrmul  20387  irredlmul  20388  isdrngrd  20726  isdrngrdOLD  20728  islmodd  20823  lmodcom  20865  rmodislmod  20887  zntoslem  21517  ipcl  21593  evls1fpws  22307  maducoevalmin1  22590  rintopn  22847  opnnei  23058  restin  23104  cnpnei  23202  cnprest  23227  ordthaus  23322  kgen2ss  23493  hausflim  23919  fclsfnflim  23965  cnpfcf  23979  opnsubg  24046  cuspcvg  24239  psmetsym  24249  xmetsym  24286  ngpdsr  24544  ngpds2r  24546  ngpds3r  24548  clmmulg  25052  cphipval2  25193  iscau2  25229  dgr1term  26217  cxpeq0  26639  cxpge0  26644  relogbzcl  26736  negsunif  28013  grpoidinvlem2  30486  grpoinvdiv  30518  nvpncan  30635  nvabs  30653  ipval2lem2  30685  dipcj  30695  diporthcom  30697  dipdi  30824  dipassr  30827  dipsubdi  30830  hlipcj  30892  hvadd32  31015  hvsub32  31026  his5  31067  hoadd32  31764  hosubsub  31798  unopf1o  31897  adj2  31915  adjvalval  31918  adjlnop  32067  leopmul2i  32116  cvntr  32273  mdsymlem5  32388  sumdmdii  32396  supxrnemnf  32745  odutos  32948  tlt2  32949  tosglblem  32954  archiabl  33196  unitdivcld  33932  bnj605  34938  bnj607  34947  fisshasheq  35137  swrdrevpfx  35139  cusgredgex  35144  acycgr1v  35171  gcd32  35766  cgrrflx  36005  cgrcom  36008  cgrcomr  36015  btwntriv1  36034  cgr3com  36071  colineartriv2  36086  segleantisym  36133  seglelin  36134  btwnoutside  36143  clsint2  36347  dissneqlem  37358  ftc1anclem5  37721  heibor1  37834  rngoidl  38048  ispridlc  38094  opltcon3b  39222  cmtcomlemN  39266  cmtcomN  39267  cmt3N  39269  cmtbr3N  39272  cvrval2  39292  cvrnbtwn4  39297  leatb  39310  atlrelat1  39339  hlatlej2  39394  hlateq  39418  hlrelat5N  39420  snatpsubN  39769  pmap11  39781  paddcom  39832  sspadd2  39835  paddss12  39838  cdleme51finvN  40575  cdleme51finvtrN  40577  cdlemeiota  40604  cdlemg2jlemOLDN  40612  cdlemg2klem  40614  cdlemg4b1  40628  cdlemg4b2  40629  trljco2  40760  tgrpabl  40770  tendoplcom  40801  cdleml6  41000  erngdvlem3-rN  41017  dia11N  41067  dib11N  41179  dih11  41284  uzindd  41990  lcmineqlem1  42042  nerabdioph  42832  monotoddzzfi  42966  fzneg  43006  jm2.19lem2  43014  ismnushort  44325  nzss  44341  sineq0ALT  44961  lincvalsng  48392  reccot  49622