Theorem 3com23 1139

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

Syntax hints:   → wi 4   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3coml  1140  3anidm13  1439  eqreu  3692  f1ofveu  7390  curry2f  8087  dfsmo2  8318  nneob  8626  nadd32  8668  f1oeng  8951  domnsymfi  9168  sdomdomtrfi  9169  domsdomtrfi  9170  php  9175  php3  9177  fodomfir  9272  suppr  9418  infdif  10164  axdclem2  10477  gchen1  10583  grumap  10766  grudomon  10775  mul32  11349  add32  11402  subsub23  11435  subadd23  11442  addsub12  11443  subsub  11461  subsub3  11463  sub32  11465  suble  11665  lesub  11666  ltsub23  11667  ltsub13  11668  ltleadd  11670  div32  11865  div13  11866  div12  11867  divdiv32  11899  cju  12191  infssuzle  12932  ioo0  13374  ico0  13395  ioc0  13396  icc0  13397  fzen  13546  modcyc  13916  expgt0  14108  expge0  14111  expge1  14112  2cshwcom  14829  shftval2  15088  abs3dif  15359  divalgb  16438  submrc  17660  mrieqv2d  17671  pltnlt  18370  pltn2lp  18371  tosso  18449  latnle  18505  latabs1  18507  lubel  18546  ipopos  18568  grpinvcnv  19048  mulgaddcom  19140  mulgneg2  19150  oppgmnd  19394  oddvdsnn0  19584  oddvds  19587  odmulg  19596  odcl2  19605  lsmcomx  19896  srgcom4  20260  srgrmhm  20268  ringcom  20326  mulgass2  20355  opprrng  20390  irredrmul  20472  irredlmul  20473  isdrngrd  20812  isdrngrdOLD  20814  islmodd  20930  lmodcom  20972  rmodislmod  20994  zntoslem  21605  ipcl  21682  evls1fpws  22429  maducoevalmin1  22709  rintopn  22966  opnnei  23177  restin  23223  cnpnei  23321  cnprest  23346  ordthaus  23441  kgen2ss  23612  hausflim  24038  fclsfnflim  24084  cnpfcf  24098  opnsubg  24165  cuspcvg  24357  psmetsym  24367  xmetsym  24404  ngpdsr  24662  ngpds2r  24664  ngpds3r  24666  clmmulg  25160  cphipval2  25300  iscau2  25336  dgr1term  26317  cxpeq0  26740  cxpge0  26745  relogbzcl  26836  negsunif  28145  oldfib  28467  grpoidinvlem2  30705  grpoinvdiv  30737  nvpncan  30854  nvabs  30872  ipval2lem2  30904  dipcj  30914  diporthcom  30916  dipdi  31043  dipassr  31046  dipsubdi  31049  hlipcj  31111  hvadd32  31234  hvsub32  31245  his5  31286  hoadd32  31983  hosubsub  32017  unopf1o  32116  adj2  32134  adjvalval  32137  adjlnop  32286  leopmul2i  32335  cvntr  32492  mdsymlem5  32607  sumdmdii  32615  supxrnemnf  32967  odutos  33143  tlt2  33144  tosglblem  33149  archiabl  33375  unitdivcld  34195  bnj605  35199  bnj607  35208  rankfilimb  35395  r1filim  35397  fisshasheq  35462  swrdrevpfx  35464  cusgredgex  35469  acycgr1v  35496  gcd32  36096  cgrrflx  36334  cgrcom  36337  cgrcomr  36344  btwntriv1  36363  cgr3com  36400  colineartriv2  36415  segleantisym  36462  seglelin  36463  btwnoutside  36472  clsint2  36686  dissneqlem  37831  ftc1anclem5  38193  heibor1  38306  rngoidl  38520  ispridlc  38566  opltcon3b  39825  cmtcomlemN  39869  cmtcomN  39870  cmt3N  39872  cmtbr3N  39875  cvrval2  39895  cvrnbtwn4  39900  leatb  39913  atlrelat1  39942  hlatlej2  39997  hlateq  40020  hlrelat5N  40022  snatpsubN  40371  pmap11  40383  paddcom  40434  sspadd2  40437  paddss12  40440  cdleme51finvN  41177  cdleme51finvtrN  41179  cdlemeiota  41206  cdlemg2jlemOLDN  41214  cdlemg2klem  41216  cdlemg4b1  41230  cdlemg4b2  41231  trljco2  41362  tgrpabl  41372  tendoplcom  41403  cdleml6  41602  erngdvlem3-rN  41619  dia11N  41669  dib11N  41781  dih11  41886  uzindd  42592  lcmineqlem1  42643  nerabdioph  43383  monotoddzzfi  43516  fzneg  43556  jm2.19lem2  43564  ismnushort  44874  nzss  44890  sineq0ALT  45509  lincvalsng  49035  reccot  50376