Theorem 3com23 1144

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3coml  1145  3anidm13  1447  eqreu  3694  f1ofveu  7413  curry2f  8109  dfsmo2  8340  nneob  8648  nadd32  8690  f1oeng  8973  domnsymfi  9191  sdomdomtrfi  9192  domsdomtrfi  9193  php  9198  php3  9200  fodomfir  9294  suppr  9439  infdif  10207  axdclem2  10519  gchen1  10625  grumap  10808  grudomon  10817  mul32  11391  add32  11444  subsub23  11477  subadd23  11484  addsub12  11485  subsub  11503  subsub3  11505  sub32  11507  suble  11707  lesub  11708  ltsub23  11709  ltsub13  11710  ltleadd  11712  div32  11907  div13  11908  div12  11909  divdiv32  11938  cju  12229  infssuzle  12971  ioo0  13413  ico0  13434  ioc0  13435  icc0  13436  fzen  13585  modcyc  13957  expgt0  14149  expge0  14152  expge1  14153  swrdrevpfx  14828  2cshwcom  14877  shftval2  15136  abs3dif  15407  divalgb  16484  submrc  17706  mrieqv2d  17717  pltnlt  18416  pltn2lp  18417  tosso  18495  latnle  18551  latabs1  18553  lubel  18592  ipopos  18614  grpinvcnv  19117  mulgaddcom  19208  mulgneg2  19218  oppgmnd  19468  oddvdsnn0  19658  oddvds  19661  odmulg  19670  odcl2  19679  lsmcomx  19970  srgcom4  20340  srgrmhm  20348  ringcom  20408  mulgass2  20438  opprrng  20473  irredrmul  20555  irredlmul  20556  isdrngrd  20919  isdrngrdOLD  20921  islmodd  21037  lmodcom  21079  rmodislmod  21101  zntoslem  21756  ipcl  21833  evls1fpws  22579  maducoevalmin1  22859  rintopn  23116  opnnei  23327  restin  23373  cnpnei  23471  cnprest  23496  ordthaus  23591  kgen2ss  23763  hausflim  24189  fclsfnflim  24235  cnpfcf  24249  opnsubg  24316  cuspcvg  24508  psmetsym  24518  xmetsym  24555  ngpdsr  24813  ngpds2r  24815  ngpds3r  24817  clmmulg  25311  cphipval2  25451  iscau2  25487  dgr1term  26468  cxpeq0  26894  cxpge0  26899  relogbzcl  26990  negsunif  28299  oldfib  28621  grpoidinvlem2  30928  grpoinvdiv  30960  nvpncan  31077  nvabs  31095  ipval2lem2  31127  dipcj  31137  diporthcom  31139  dipdi  31266  dipassr  31269  dipsubdi  31272  hlipcj  31334  hvadd32  31457  hvsub32  31468  his5  31509  hoadd32  32206  hosubsub  32240  unopf1o  32339  adj2  32357  adjvalval  32360  adjlnop  32509  leopmul2i  32558  cvntr  32715  mdsymlem5  32830  sumdmdii  32838  supxrnemnf  33183  odutos  33352  tlt2  33353  tosglblem  33358  archiabl  33582  unitdivcld  34355  bnj605  35360  bnj607  35369  rankfilimb  35554  r1filim  35556  fisshasheq  35661  cusgredgex  35664  acycgr1v  35678  gcd32  36278  cgrrflx  36516  cgrcom  36519  cgrcomr  36526  btwntriv1  36545  cgr3com  36582  colineartriv2  36597  segleantisym  36644  seglelin  36645  btwnoutside  36654  clsint2  36897  dissneqlem  38043  ftc1anclem5  38405  heibor1  38519  rngoidl  38733  ispridlc  38779  opltcon3b  40036  cmtcomlemN  40080  cmtcomN  40081  cmt3N  40083  cmtbr3N  40086  cvrval2  40106  cvrnbtwn4  40111  leatb  40124  atlrelat1  40153  hlatlej2  40208  hlateq  40231  hlrelat5N  40233  snatpsubN  40582  pmap11  40594  paddcom  40645  sspadd2  40648  paddss12  40651  cdleme51finvN  41388  cdleme51finvtrN  41390  cdlemeiota  41417  cdlemg2jlemOLDN  41425  cdlemg2klem  41427  cdlemg4b1  41441  cdlemg4b2  41442  trljco2  41573  tgrpabl  41583  tendoplcom  41614  cdleml6  41813  erngdvlem3-rN  41830  dia11N  41880  dib11N  41992  dih11  42097  uzindd  42803  lcmineqlem1  42854  nerabdioph  43594  monotoddzzfi  43727  fzneg  43767  jm2.19lem2  43775  ismnushort  45069  nzss  45085  sineq0ALT  45703  lincvalsng  49253  reccot  50593