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 1087

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 1089

This theorem is referenced by:  3coml  1127  3anidm13  1420  eqreu  3751  f1ofveu  7442  curry2f  8149  dfsmo2  8403  nneob  8712  nadd32  8753  f1oeng  9031  domnsymfi  9266  sdomdomtrfi  9267  domsdomtrfi  9268  php  9273  php3  9275  fodomfir  9396  suppr  9540  infdif  10277  axdclem2  10589  gchen1  10694  grumap  10877  grudomon  10886  mul32  11456  add32  11508  subsub23  11541  subadd23  11548  addsub12  11549  subsub  11566  subsub3  11568  sub32  11570  suble  11768  lesub  11769  ltsub23  11770  ltsub13  11771  ltleadd  11773  div32  11969  div13  11970  div12  11971  divdiv32  12002  cju  12289  infssuzle  12996  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  fzen  13601  modcyc  13957  expgt0  14146  expge0  14149  expge1  14150  2cshwcom  14864  shftval2  15124  abs3dif  15380  divalgb  16452  submrc  17686  mrieqv2d  17697  pltnlt  18410  pltn2lp  18411  tosso  18489  latnle  18543  latabs1  18545  lubel  18584  ipopos  18606  grpinvcnv  19046  mulgaddcom  19138  mulgneg2  19148  oppgmnd  19397  oddvdsnn0  19586  oddvds  19589  odmulg  19598  odcl2  19607  lsmcomx  19898  srgcom4  20241  srgrmhm  20249  ringcom  20303  mulgass2  20332  opprrng  20371  irredrmul  20453  irredlmul  20454  isdrngrd  20788  isdrngrdOLD  20790  islmodd  20886  lmodcom  20928  rmodislmod  20950  rmodislmodOLD  20951  zntoslem  21598  ipcl  21674  evls1fpws  22394  maducoevalmin1  22679  rintopn  22936  opnnei  23149  restin  23195  cnpnei  23293  cnprest  23318  ordthaus  23413  kgen2ss  23584  hausflim  24010  fclsfnflim  24056  cnpfcf  24070  opnsubg  24137  cuspcvg  24331  psmetsym  24341  xmetsym  24378  ngpdsr  24639  ngpds2r  24641  ngpds3r  24643  clmmulg  25153  cphipval2  25294  iscau2  25330  dgr1term  26319  cxpeq0  26738  cxpge0  26743  relogbzcl  26835  negsunif  28105  grpoidinvlem2  30537  grpoinvdiv  30569  nvpncan  30686  nvabs  30704  ipval2lem2  30736  dipcj  30746  diporthcom  30748  dipdi  30875  dipassr  30878  dipsubdi  30881  hlipcj  30943  hvadd32  31066  hvsub32  31077  his5  31118  hoadd32  31815  hosubsub  31849  unopf1o  31948  adj2  31966  adjvalval  31969  adjlnop  32118  leopmul2i  32167  cvntr  32324  mdsymlem5  32439  sumdmdii  32447  supxrnemnf  32775  odutos  32941  tlt2  32942  tosglblem  32947  archiabl  33178  unitdivcld  33847  bnj605  34883  bnj607  34892  fisshasheq  35082  swrdrevpfx  35084  cusgredgex  35089  acycgr1v  35117  gcd32  35711  cgrrflx  35951  cgrcom  35954  cgrcomr  35961  btwntriv1  35980  cgr3com  36017  colineartriv2  36032  segleantisym  36079  seglelin  36080  btwnoutside  36089  clsint2  36295  dissneqlem  37306  ftc1anclem5  37657  heibor1  37770  rngoidl  37984  ispridlc  38030  opltcon3b  39160  cmtcomlemN  39204  cmtcomN  39205  cmt3N  39207  cmtbr3N  39210  cvrval2  39230  cvrnbtwn4  39235  leatb  39248  atlrelat1  39277  hlatlej2  39332  hlateq  39356  hlrelat5N  39358  snatpsubN  39707  pmap11  39719  paddcom  39770  sspadd2  39773  paddss12  39776  cdleme51finvN  40513  cdleme51finvtrN  40515  cdlemeiota  40542  cdlemg2jlemOLDN  40550  cdlemg2klem  40552  cdlemg4b1  40566  cdlemg4b2  40567  trljco2  40698  tgrpabl  40708  tendoplcom  40739  cdleml6  40938  erngdvlem3-rN  40955  dia11N  41005  dib11N  41117  dih11  41222  uzindd  41933  lcmineqlem1  41986  nerabdioph  42765  monotoddzzfi  42899  fzneg  42939  jm2.19lem2  42947  ismnushort  44270  nzss  44286  sineq0ALT  44908  lincvalsng  48145  reccot  48850