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  3722  f1ofveu  7153  curry2f  7805  dfsmo2  7986  nneob  8281  f1oeng  8530  suppr  8937  infdif  9633  axdclem2  9944  gchen1  10049  grumap  10232  grudomon  10241  mul32  10808  add32  10860  subsub23  10893  subadd23  10900  addsub12  10901  subsub  10918  subsub3  10920  sub32  10922  suble  11120  lesub  11121  ltsub23  11122  ltsub13  11123  ltleadd  11125  div32  11320  div13  11321  div12  11322  divdiv32  11350  cju  11636  infssuzle  12334  ioo0  12766  ico0  12787  ioc0  12788  icc0  12789  fzen  12927  modcyc  13277  expgt0  13465  expge0  13468  expge1  13469  2cshwcom  14180  shftval2  14436  abs3dif  14693  divalgb  15757  submrc  16901  mrieqv2d  16912  pltnlt  17580  pltn2lp  17581  tosso  17648  latnle  17697  latabs1  17699  lubel  17734  ipopos  17772  grpinvcnv  18169  mulgaddcom  18253  mulgneg2  18263  oppgmnd  18484  oddvdsnn0  18674  oddvds  18677  odmulg  18685  odcl2  18694  lsmcomx  18978  srgrmhm  19288  ringcom  19331  mulgass2  19353  opprring  19383  irredrmul  19459  irredlmul  19460  isdrngrd  19530  islmodd  19642  lmodcom  19682  rmodislmod  19704  opprdomn  20076  zntoslem  20705  ipcl  20779  maducoevalmin1  21263  rintopn  21519  opnnei  21730  restin  21776  cnpnei  21874  cnprest  21899  ordthaus  21994  kgen2ss  22165  hausflim  22591  fclsfnflim  22637  cnpfcf  22651  opnsubg  22718  cuspcvg  22912  psmetsym  22922  xmetsym  22959  ngpdsr  23216  ngpds2r  23218  ngpds3r  23220  clmmulg  23707  cphipval2  23846  iscau2  23882  dgr1term  24852  cxpeq0  25263  cxpge0  25268  relogbzcl  25354  grpoidinvlem2  28284  grpoinvdiv  28316  nvpncan  28433  nvabs  28451  ipval2lem2  28483  dipcj  28493  diporthcom  28495  dipdi  28622  dipassr  28625  dipsubdi  28628  hlipcj  28690  hvadd32  28813  hvsub32  28824  his5  28865  hoadd32  29562  hosubsub  29596  unopf1o  29695  adj2  29713  adjvalval  29716  adjlnop  29865  leopmul2i  29914  cvntr  30071  mdsymlem5  30186  sumdmdii  30194  supxrnemnf  30495  odutos  30652  tlt2  30653  tosglblem  30658  archiabl  30829  unitdivcld  31146  bnj605  32181  bnj607  32190  fisshasheq  32354  swrdrevpfx  32365  cusgredgex  32370  acycgr1v  32398  gcd32  32985  cgrrflx  33450  cgrcom  33453  cgrcomr  33460  btwntriv1  33479  cgr3com  33516  colineartriv2  33531  segleantisym  33578  seglelin  33579  btwnoutside  33588  clsint2  33679  dissneqlem  34623  ftc1anclem5  34973  heibor1  35090  rngoidl  35304  ispridlc  35350  opltcon3b  36342  cmtcomlemN  36386  cmtcomN  36387  cmt3N  36389  cmtbr3N  36392  cvrval2  36412  cvrnbtwn4  36417  leatb  36430  atlrelat1  36459  hlatlej2  36514  hlateq  36537  hlrelat5N  36539  snatpsubN  36888  pmap11  36900  paddcom  36951  sspadd2  36954  paddss12  36957  cdleme51finvN  37694  cdleme51finvtrN  37696  cdlemeiota  37723  cdlemg2jlemOLDN  37731  cdlemg2klem  37733  cdlemg4b1  37747  cdlemg4b2  37748  trljco2  37879  tgrpabl  37889  tendoplcom  37920  cdleml6  38119  erngdvlem3-rN  38136  dia11N  38186  dib11N  38298  dih11  38403  nerabdioph  39413  monotoddzzfi  39546  fzneg  39586  jm2.19lem2  39594  nzss  40656  sineq0ALT  41278  lincvalsng  44478  reccot  44864