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

This theorem is referenced by:  3coml  1126  3anidm13  1419  eqreu  3737  f1ofveu  7424  curry2f  8131  dfsmo2  8385  nneob  8692  nadd32  8733  f1oeng  9009  domnsymfi  9237  sdomdomtrfi  9238  domsdomtrfi  9239  php  9244  php3  9246  fodomfir  9365  suppr  9508  infdif  10245  axdclem2  10557  gchen1  10662  grumap  10845  grudomon  10854  mul32  11424  add32  11477  subsub23  11510  subadd23  11517  addsub12  11518  subsub  11536  subsub3  11538  sub32  11540  suble  11738  lesub  11739  ltsub23  11740  ltsub13  11741  ltleadd  11743  div32  11939  div13  11940  div12  11941  divdiv32  11972  cju  12259  infssuzle  12970  ioo0  13408  ico0  13429  ioc0  13430  icc0  13431  fzen  13577  modcyc  13942  expgt0  14132  expge0  14135  expge1  14136  2cshwcom  14850  shftval2  15110  abs3dif  15366  divalgb  16437  submrc  17672  mrieqv2d  17683  pltnlt  18397  pltn2lp  18398  tosso  18476  latnle  18530  latabs1  18532  lubel  18571  ipopos  18593  grpinvcnv  19036  mulgaddcom  19128  mulgneg2  19138  oppgmnd  19387  oddvdsnn0  19576  oddvds  19579  odmulg  19588  odcl2  19597  lsmcomx  19888  srgcom4  20231  srgrmhm  20239  ringcom  20293  mulgass2  20322  opprrng  20361  irredrmul  20443  irredlmul  20444  isdrngrd  20782  isdrngrdOLD  20784  islmodd  20880  lmodcom  20922  rmodislmod  20944  rmodislmodOLD  20945  zntoslem  21592  ipcl  21668  evls1fpws  22388  maducoevalmin1  22673  rintopn  22930  opnnei  23143  restin  23189  cnpnei  23287  cnprest  23312  ordthaus  23407  kgen2ss  23578  hausflim  24004  fclsfnflim  24050  cnpfcf  24064  opnsubg  24131  cuspcvg  24325  psmetsym  24335  xmetsym  24372  ngpdsr  24633  ngpds2r  24635  ngpds3r  24637  clmmulg  25147  cphipval2  25288  iscau2  25324  dgr1term  26313  cxpeq0  26734  cxpge0  26739  relogbzcl  26831  negsunif  28101  grpoidinvlem2  30533  grpoinvdiv  30565  nvpncan  30682  nvabs  30700  ipval2lem2  30732  dipcj  30742  diporthcom  30744  dipdi  30871  dipassr  30874  dipsubdi  30877  hlipcj  30939  hvadd32  31062  hvsub32  31073  his5  31114  hoadd32  31811  hosubsub  31845  unopf1o  31944  adj2  31962  adjvalval  31965  adjlnop  32114  leopmul2i  32163  cvntr  32320  mdsymlem5  32435  sumdmdii  32443  supxrnemnf  32778  odutos  32942  tlt2  32943  tosglblem  32948  archiabl  33187  unitdivcld  33861  bnj605  34899  bnj607  34908  fisshasheq  35098  swrdrevpfx  35100  cusgredgex  35105  acycgr1v  35133  gcd32  35728  cgrrflx  35968  cgrcom  35971  cgrcomr  35978  btwntriv1  35997  cgr3com  36034  colineartriv2  36049  segleantisym  36096  seglelin  36097  btwnoutside  36106  clsint2  36311  dissneqlem  37322  ftc1anclem5  37683  heibor1  37796  rngoidl  38010  ispridlc  38056  opltcon3b  39185  cmtcomlemN  39229  cmtcomN  39230  cmt3N  39232  cmtbr3N  39235  cvrval2  39255  cvrnbtwn4  39260  leatb  39273  atlrelat1  39302  hlatlej2  39357  hlateq  39381  hlrelat5N  39383  snatpsubN  39732  pmap11  39744  paddcom  39795  sspadd2  39798  paddss12  39801  cdleme51finvN  40538  cdleme51finvtrN  40540  cdlemeiota  40567  cdlemg2jlemOLDN  40575  cdlemg2klem  40577  cdlemg4b1  40591  cdlemg4b2  40592  trljco2  40723  tgrpabl  40733  tendoplcom  40764  cdleml6  40963  erngdvlem3-rN  40980  dia11N  41030  dib11N  41142  dih11  41247  uzindd  41958  lcmineqlem1  42010  nerabdioph  42796  monotoddzzfi  42930  fzneg  42970  jm2.19lem2  42978  ismnushort  44296  nzss  44312  sineq0ALT  44934  lincvalsng  48261  reccot  48988