Theorem 3com23 1122

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3coml  1123  3anidm13  1416  eqreu  3719  f1ofveu  7150  curry2f  7802  dfsmo2  7983  nneob  8278  f1oeng  8527  suppr  8934  infdif  9630  axdclem2  9941  gchen1  10046  grumap  10229  grudomon  10238  mul32  10805  add32  10857  subsub23  10890  subadd23  10897  addsub12  10898  subsub  10915  subsub3  10917  sub32  10919  suble  11117  lesub  11118  ltsub23  11119  ltsub13  11120  ltleadd  11122  div32  11317  div13  11318  div12  11319  divdiv32  11347  cju  11633  infssuzle  12330  ioo0  12762  ico0  12783  ioc0  12784  icc0  12785  fzen  12923  modcyc  13273  expgt0  13461  expge0  13464  expge1  13465  2cshwcom  14177  shftval2  14433  abs3dif  14690  divalgb  15754  submrc  16898  mrieqv2d  16909  pltnlt  17577  pltn2lp  17578  tosso  17645  latnle  17694  latabs1  17696  lubel  17731  ipopos  17769  grpinvcnv  18166  mulgaddcom  18250  mulgneg2  18260  oppgmnd  18481  oddvdsnn0  18671  oddvds  18674  odmulg  18682  odcl2  18691  lsmcomx  18975  srgrmhm  19285  ringcom  19328  mulgass2  19350  opprring  19380  irredrmul  19456  irredlmul  19457  isdrngrd  19527  islmodd  19639  lmodcom  19679  rmodislmod  19701  opprdomn  20073  zntoslem  20702  ipcl  20776  maducoevalmin1  21260  rintopn  21516  opnnei  21727  restin  21773  cnpnei  21871  cnprest  21896  ordthaus  21991  kgen2ss  22162  hausflim  22588  fclsfnflim  22634  cnpfcf  22648  opnsubg  22715  cuspcvg  22909  psmetsym  22919  xmetsym  22956  ngpdsr  23213  ngpds2r  23215  ngpds3r  23217  clmmulg  23704  cphipval2  23843  iscau2  23879  dgr1term  24849  cxpeq0  25260  cxpge0  25265  relogbzcl  25351  grpoidinvlem2  28281  grpoinvdiv  28313  nvpncan  28430  nvabs  28448  ipval2lem2  28480  dipcj  28490  diporthcom  28492  dipdi  28619  dipassr  28622  dipsubdi  28625  hlipcj  28687  hvadd32  28810  hvsub32  28821  his5  28862  hoadd32  29559  hosubsub  29593  unopf1o  29692  adj2  29710  adjvalval  29713  adjlnop  29862  leopmul2i  29911  cvntr  30068  mdsymlem5  30183  sumdmdii  30191  supxrnemnf  30492  odutos  30650  tlt2  30651  tosglblem  30656  archiabl  30827  unitdivcld  31144  bnj605  32179  bnj607  32188  fisshasheq  32352  swrdrevpfx  32363  cusgredgex  32368  acycgr1v  32396  gcd32  32983  cgrrflx  33448  cgrcom  33451  cgrcomr  33458  btwntriv1  33477  cgr3com  33514  colineartriv2  33529  segleantisym  33576  seglelin  33577  btwnoutside  33586  clsint2  33677  dissneqlem  34620  ftc1anclem5  34970  heibor1  35087  rngoidl  35301  ispridlc  35347  opltcon3b  36339  cmtcomlemN  36383  cmtcomN  36384  cmt3N  36386  cmtbr3N  36389  cvrval2  36409  cvrnbtwn4  36414  leatb  36427  atlrelat1  36456  hlatlej2  36511  hlateq  36534  hlrelat5N  36536  snatpsubN  36885  pmap11  36897  paddcom  36948  sspadd2  36951  paddss12  36954  cdleme51finvN  37691  cdleme51finvtrN  37693  cdlemeiota  37720  cdlemg2jlemOLDN  37728  cdlemg2klem  37730  cdlemg4b1  37744  cdlemg4b2  37745  trljco2  37876  tgrpabl  37886  tendoplcom  37917  cdleml6  38116  erngdvlem3-rN  38133  dia11N  38183  dib11N  38295  dih11  38400  nerabdioph  39404  monotoddzzfi  39537  fzneg  39577  jm2.19lem2  39585  nzss  40647  sineq0ALT  41269  lincvalsng  44470  reccot  44856