Theorem 3com23 1125

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  3coml  1126  3anidm13  1419  eqreu  3668  f1ofveu  7266  curry2f  7939  dfsmo2  8169  nneob  8469  f1oeng  8742  domnsymfi  8968  sdomdomtrfi  8969  domsdomtrfi  8970  php  8974  php3  8976  suppr  9208  infdif  9966  axdclem2  10277  gchen1  10382  grumap  10565  grudomon  10574  mul32  11141  add32  11193  subsub23  11226  subadd23  11233  addsub12  11234  subsub  11251  subsub3  11253  sub32  11255  suble  11453  lesub  11454  ltsub23  11455  ltsub13  11456  ltleadd  11458  div32  11653  div13  11654  div12  11655  divdiv32  11683  cju  11969  infssuzle  12670  ioo0  13103  ico0  13124  ioc0  13125  icc0  13126  fzen  13272  modcyc  13624  expgt0  13814  expge0  13817  expge1  13818  2cshwcom  14527  shftval2  14784  abs3dif  15041  divalgb  16111  submrc  17335  mrieqv2d  17346  pltnlt  18056  pltn2lp  18057  tosso  18135  latnle  18189  latabs1  18191  lubel  18230  ipopos  18252  grpinvcnv  18641  mulgaddcom  18725  mulgneg2  18735  oppgmnd  18959  oddvdsnn0  19150  oddvds  19153  odmulg  19161  odcl2  19170  lsmcomx  19455  srgrmhm  19770  ringcom  19816  mulgass2  19838  opprring  19871  irredrmul  19947  irredlmul  19948  isdrngrd  20015  islmodd  20127  lmodcom  20167  rmodislmod  20189  rmodislmodOLD  20190  opprdomn  20570  zntoslem  20762  ipcl  20836  maducoevalmin1  21799  rintopn  22056  opnnei  22269  restin  22315  cnpnei  22413  cnprest  22438  ordthaus  22533  kgen2ss  22704  hausflim  23130  fclsfnflim  23176  cnpfcf  23190  opnsubg  23257  cuspcvg  23451  psmetsym  23461  xmetsym  23498  ngpdsr  23759  ngpds2r  23761  ngpds3r  23763  clmmulg  24262  cphipval2  24403  iscau2  24439  dgr1term  25419  cxpeq0  25831  cxpge0  25836  relogbzcl  25922  grpoidinvlem2  28863  grpoinvdiv  28895  nvpncan  29012  nvabs  29030  ipval2lem2  29062  dipcj  29072  diporthcom  29074  dipdi  29201  dipassr  29204  dipsubdi  29207  hlipcj  29269  hvadd32  29392  hvsub32  29403  his5  29444  hoadd32  30141  hosubsub  30175  unopf1o  30274  adj2  30292  adjvalval  30295  adjlnop  30444  leopmul2i  30493  cvntr  30650  mdsymlem5  30765  sumdmdii  30773  supxrnemnf  31087  odutos  31242  tlt2  31243  tosglblem  31248  archiabl  31448  unitdivcld  31847  bnj605  32883  bnj607  32892  fisshasheq  33069  swrdrevpfx  33074  cusgredgex  33079  acycgr1v  33107  gcd32  33711  cgrrflx  34285  cgrcom  34288  cgrcomr  34295  btwntriv1  34314  cgr3com  34351  colineartriv2  34366  segleantisym  34413  seglelin  34414  btwnoutside  34423  clsint2  34514  dissneqlem  35507  ftc1anclem5  35850  heibor1  35964  rngoidl  36178  ispridlc  36224  opltcon3b  37214  cmtcomlemN  37258  cmtcomN  37259  cmt3N  37261  cmtbr3N  37264  cvrval2  37284  cvrnbtwn4  37289  leatb  37302  atlrelat1  37331  hlatlej2  37386  hlateq  37409  hlrelat5N  37411  snatpsubN  37760  pmap11  37772  paddcom  37823  sspadd2  37826  paddss12  37829  cdleme51finvN  38566  cdleme51finvtrN  38568  cdlemeiota  38595  cdlemg2jlemOLDN  38603  cdlemg2klem  38605  cdlemg4b1  38619  cdlemg4b2  38620  trljco2  38751  tgrpabl  38761  tendoplcom  38792  cdleml6  38991  erngdvlem3-rN  39008  dia11N  39058  dib11N  39170  dih11  39275  uzindd  39982  lcmineqlem1  40034  nerabdioph  40628  monotoddzzfi  40761  fzneg  40801  jm2.19lem2  40809  ismnushort  41889  nzss  41905  sineq0ALT  42527  lincvalsng  45726  reccot  46429