Theorem 3com23 1123

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3coml  1124  3anidm13  1417  eqreu  3668  f1ofveu  7130  curry2f  7786  dfsmo2  7967  nneob  8262  f1oeng  8511  suppr  8919  infdif  9620  axdclem2  9931  gchen1  10036  grumap  10219  grudomon  10228  mul32  10795  add32  10847  subsub23  10880  subadd23  10887  addsub12  10888  subsub  10905  subsub3  10907  sub32  10909  suble  11107  lesub  11108  ltsub23  11109  ltsub13  11110  ltleadd  11112  div32  11307  div13  11308  div12  11309  divdiv32  11337  cju  11621  infssuzle  12319  ioo0  12751  ico0  12772  ioc0  12773  icc0  12774  fzen  12919  modcyc  13269  expgt0  13458  expge0  13461  expge1  13462  2cshwcom  14169  shftval2  14426  abs3dif  14683  divalgb  15745  submrc  16891  mrieqv2d  16902  pltnlt  17570  pltn2lp  17571  tosso  17638  latnle  17687  latabs1  17689  lubel  17724  ipopos  17762  grpinvcnv  18159  mulgaddcom  18243  mulgneg2  18253  oppgmnd  18474  oddvdsnn0  18664  oddvds  18667  odmulg  18675  odcl2  18684  lsmcomx  18969  srgrmhm  19279  ringcom  19325  mulgass2  19347  opprring  19377  irredrmul  19453  irredlmul  19454  isdrngrd  19521  islmodd  19633  lmodcom  19673  rmodislmod  19695  opprdomn  20067  zntoslem  20248  ipcl  20322  maducoevalmin1  21257  rintopn  21514  opnnei  21725  restin  21771  cnpnei  21869  cnprest  21894  ordthaus  21989  kgen2ss  22160  hausflim  22586  fclsfnflim  22632  cnpfcf  22646  opnsubg  22713  cuspcvg  22907  psmetsym  22917  xmetsym  22954  ngpdsr  23211  ngpds2r  23213  ngpds3r  23215  clmmulg  23706  cphipval2  23845  iscau2  23881  dgr1term  24857  cxpeq0  25269  cxpge0  25274  relogbzcl  25360  grpoidinvlem2  28288  grpoinvdiv  28320  nvpncan  28437  nvabs  28455  ipval2lem2  28487  dipcj  28497  diporthcom  28499  dipdi  28626  dipassr  28629  dipsubdi  28632  hlipcj  28694  hvadd32  28817  hvsub32  28828  his5  28869  hoadd32  29566  hosubsub  29600  unopf1o  29699  adj2  29717  adjvalval  29720  adjlnop  29869  leopmul2i  29918  cvntr  30075  mdsymlem5  30190  sumdmdii  30198  supxrnemnf  30519  odutos  30676  tlt2  30677  tosglblem  30682  archiabl  30877  unitdivcld  31254  bnj605  32289  bnj607  32298  fisshasheq  32462  swrdrevpfx  32476  cusgredgex  32481  acycgr1v  32509  gcd32  33096  cgrrflx  33561  cgrcom  33564  cgrcomr  33571  btwntriv1  33590  cgr3com  33627  colineartriv2  33642  segleantisym  33689  seglelin  33690  btwnoutside  33699  clsint2  33790  dissneqlem  34757  ftc1anclem5  35134  heibor1  35248  rngoidl  35462  ispridlc  35508  opltcon3b  36500  cmtcomlemN  36544  cmtcomN  36545  cmt3N  36547  cmtbr3N  36550  cvrval2  36570  cvrnbtwn4  36575  leatb  36588  atlrelat1  36617  hlatlej2  36672  hlateq  36695  hlrelat5N  36697  snatpsubN  37046  pmap11  37058  paddcom  37109  sspadd2  37112  paddss12  37115  cdleme51finvN  37852  cdleme51finvtrN  37854  cdlemeiota  37881  cdlemg2jlemOLDN  37889  cdlemg2klem  37891  cdlemg4b1  37905  cdlemg4b2  37906  trljco2  38037  tgrpabl  38047  tendoplcom  38078  cdleml6  38277  erngdvlem3-rN  38294  dia11N  38344  dib11N  38456  dih11  38561  uzindd  39264  lcmineqlem1  39317  nerabdioph  39750  monotoddzzfi  39883  fzneg  39923  jm2.19lem2  39931  nzss  41021  sineq0ALT  41643  lincvalsng  44825  reccot  45284