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

This theorem is referenced by:  3coml  1127  3anidm13  1422  eqreu  3697  f1ofveu  7363  curry2f  8064  dfsmo2  8293  nneob  8597  nadd32  8638  f1oeng  8919  domnsymfi  9141  sdomdomtrfi  9142  domsdomtrfi  9143  php  9148  php3  9150  fodomfir  9255  suppr  9399  infdif  10137  axdclem2  10449  gchen1  10554  grumap  10737  grudomon  10746  mul32  11316  add32  11369  subsub23  11402  subadd23  11409  addsub12  11410  subsub  11428  subsub3  11430  sub32  11432  suble  11632  lesub  11633  ltsub23  11634  ltsub13  11635  ltleadd  11637  div32  11833  div13  11834  div12  11835  divdiv32  11866  cju  12158  infssuzle  12866  ioo0  13307  ico0  13328  ioc0  13329  icc0  13330  fzen  13478  modcyc  13844  expgt0  14036  expge0  14039  expge1  14040  2cshwcom  14757  shftval2  15017  abs3dif  15274  divalgb  16350  submrc  17569  mrieqv2d  17580  pltnlt  18279  pltn2lp  18280  tosso  18358  latnle  18414  latabs1  18416  lubel  18455  ipopos  18477  grpinvcnv  18920  mulgaddcom  19012  mulgneg2  19022  oppgmnd  19268  oddvdsnn0  19458  oddvds  19461  odmulg  19470  odcl2  19479  lsmcomx  19770  srgcom4  20134  srgrmhm  20142  ringcom  20200  mulgass2  20229  opprrng  20265  irredrmul  20347  irredlmul  20348  isdrngrd  20686  isdrngrdOLD  20688  islmodd  20804  lmodcom  20846  rmodislmod  20868  zntoslem  21498  ipcl  21575  evls1fpws  22289  maducoevalmin1  22572  rintopn  22829  opnnei  23040  restin  23086  cnpnei  23184  cnprest  23209  ordthaus  23304  kgen2ss  23475  hausflim  23901  fclsfnflim  23947  cnpfcf  23961  opnsubg  24028  cuspcvg  24221  psmetsym  24231  xmetsym  24268  ngpdsr  24526  ngpds2r  24528  ngpds3r  24530  clmmulg  25034  cphipval2  25174  iscau2  25210  dgr1term  26198  cxpeq0  26620  cxpge0  26625  relogbzcl  26717  negsunif  28001  grpoidinvlem2  30484  grpoinvdiv  30516  nvpncan  30633  nvabs  30651  ipval2lem2  30683  dipcj  30693  diporthcom  30695  dipdi  30822  dipassr  30825  dipsubdi  30828  hlipcj  30890  hvadd32  31013  hvsub32  31024  his5  31065  hoadd32  31762  hosubsub  31796  unopf1o  31895  adj2  31913  adjvalval  31916  adjlnop  32065  leopmul2i  32114  cvntr  32271  mdsymlem5  32386  sumdmdii  32394  supxrnemnf  32741  odutos  32940  tlt2  32941  tosglblem  32946  archiabl  33167  unitdivcld  33884  bnj605  34890  bnj607  34899  fisshasheq  35095  swrdrevpfx  35097  cusgredgex  35102  acycgr1v  35129  gcd32  35729  cgrrflx  35968  cgrcom  35971  cgrcomr  35978  btwntriv1  35997  cgr3com  36034  colineartriv2  36049  segleantisym  36096  seglelin  36097  btwnoutside  36106  clsint2  36310  dissneqlem  37321  ftc1anclem5  37684  heibor1  37797  rngoidl  38011  ispridlc  38057  opltcon3b  39190  cmtcomlemN  39234  cmtcomN  39235  cmt3N  39237  cmtbr3N  39240  cvrval2  39260  cvrnbtwn4  39265  leatb  39278  atlrelat1  39307  hlatlej2  39362  hlateq  39386  hlrelat5N  39388  snatpsubN  39737  pmap11  39749  paddcom  39800  sspadd2  39803  paddss12  39806  cdleme51finvN  40543  cdleme51finvtrN  40545  cdlemeiota  40572  cdlemg2jlemOLDN  40580  cdlemg2klem  40582  cdlemg4b1  40596  cdlemg4b2  40597  trljco2  40728  tgrpabl  40738  tendoplcom  40769  cdleml6  40968  erngdvlem3-rN  40985  dia11N  41035  dib11N  41147  dih11  41252  uzindd  41958  lcmineqlem1  42010  nerabdioph  42790  monotoddzzfi  42924  fzneg  42964  jm2.19lem2  42972  ismnushort  44283  nzss  44299  sineq0ALT  44919  lincvalsng  48398  reccot  49740