Theorem 3com23 1124

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3coml  1125  3anidm13  1418  eqreu  3722  f1ofveu  7408  curry2f  8107  dfsmo2  8361  nneob  8670  nadd32  8711  f1oeng  8983  domnsymfi  9219  sdomdomtrfi  9220  domsdomtrfi  9221  php  9226  php3  9228  suppr  9486  infdif  10224  axdclem2  10535  gchen1  10640  grumap  10823  grudomon  10832  mul32  11402  add32  11454  subsub23  11487  subadd23  11494  addsub12  11495  subsub  11512  subsub3  11514  sub32  11516  suble  11714  lesub  11715  ltsub23  11716  ltsub13  11717  ltleadd  11719  div32  11914  div13  11915  div12  11916  divdiv32  11944  cju  12230  infssuzle  12937  ioo0  13373  ico0  13394  ioc0  13395  icc0  13396  fzen  13542  modcyc  13895  expgt0  14084  expge0  14087  expge1  14088  2cshwcom  14790  shftval2  15046  abs3dif  15302  divalgb  16372  submrc  17599  mrieqv2d  17610  pltnlt  18323  pltn2lp  18324  tosso  18402  latnle  18456  latabs1  18458  lubel  18497  ipopos  18519  grpinvcnv  18954  mulgaddcom  19044  mulgneg2  19054  oppgmnd  19299  oddvdsnn0  19490  oddvds  19493  odmulg  19502  odcl2  19511  lsmcomx  19802  srgcom4  20145  srgrmhm  20153  ringcom  20205  mulgass2  20234  opprrng  20273  irredrmul  20355  irredlmul  20356  isdrngrd  20647  isdrngrdOLD  20649  islmodd  20738  lmodcom  20780  rmodislmod  20802  rmodislmodOLD  20803  opprdomn  21239  zntoslem  21477  ipcl  21552  maducoevalmin1  22541  rintopn  22798  opnnei  23011  restin  23057  cnpnei  23155  cnprest  23180  ordthaus  23275  kgen2ss  23446  hausflim  23872  fclsfnflim  23918  cnpfcf  23932  opnsubg  23999  cuspcvg  24193  psmetsym  24203  xmetsym  24240  ngpdsr  24501  ngpds2r  24503  ngpds3r  24505  clmmulg  25015  cphipval2  25156  iscau2  25192  dgr1term  26181  cxpeq0  26599  cxpge0  26604  relogbzcl  26693  negsunif  27954  grpoidinvlem2  30302  grpoinvdiv  30334  nvpncan  30451  nvabs  30469  ipval2lem2  30501  dipcj  30511  diporthcom  30513  dipdi  30640  dipassr  30643  dipsubdi  30646  hlipcj  30708  hvadd32  30831  hvsub32  30842  his5  30883  hoadd32  31580  hosubsub  31614  unopf1o  31713  adj2  31731  adjvalval  31734  adjlnop  31883  leopmul2i  31932  cvntr  32089  mdsymlem5  32204  sumdmdii  32212  supxrnemnf  32522  odutos  32677  tlt2  32678  tosglblem  32683  archiabl  32884  evls1fpws  33182  unitdivcld  33438  bnj605  34474  bnj607  34483  fisshasheq  34660  swrdrevpfx  34662  cusgredgex  34667  acycgr1v  34695  gcd32  35279  cgrrflx  35519  cgrcom  35522  cgrcomr  35529  btwntriv1  35548  cgr3com  35585  colineartriv2  35600  segleantisym  35647  seglelin  35648  btwnoutside  35657  clsint2  35749  dissneqlem  36755  ftc1anclem5  37105  heibor1  37218  rngoidl  37432  ispridlc  37478  opltcon3b  38613  cmtcomlemN  38657  cmtcomN  38658  cmt3N  38660  cmtbr3N  38663  cvrval2  38683  cvrnbtwn4  38688  leatb  38701  atlrelat1  38730  hlatlej2  38785  hlateq  38809  hlrelat5N  38811  snatpsubN  39160  pmap11  39172  paddcom  39223  sspadd2  39226  paddss12  39229  cdleme51finvN  39966  cdleme51finvtrN  39968  cdlemeiota  39995  cdlemg2jlemOLDN  40003  cdlemg2klem  40005  cdlemg4b1  40019  cdlemg4b2  40020  trljco2  40151  tgrpabl  40161  tendoplcom  40192  cdleml6  40391  erngdvlem3-rN  40408  dia11N  40458  dib11N  40570  dih11  40675  uzindd  41384  lcmineqlem1  41437  nerabdioph  42151  monotoddzzfi  42285  fzneg  42325  jm2.19lem2  42333  ismnushort  43661  nzss  43677  sineq0ALT  44299  lincvalsng  47407  reccot  48112