Theorem 3com23 1144

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3coml  1145  3anidm13  1447  eqreu  3687  f1ofveu  7407  curry2f  8105  dfsmo2  8336  nneob  8644  nadd32  8686  f1oeng  8976  domnsymfi  9194  sdomdomtrfi  9195  domsdomtrfi  9196  php  9201  php3  9203  fodomfir  9297  suppr  9442  infdif  10210  axdclem2  10522  gchen1  10634  grumap  10817  grudomon  10826  mul32  11400  add32  11453  subsub23  11486  subadd23  11493  addsub12  11494  subsub  11512  subsub3  11514  sub32  11516  suble  11716  lesub  11717  ltsub23  11718  ltsub13  11719  ltleadd  11721  div32  11916  div13  11917  div12  11918  divdiv32  11947  cju  12238  infssuzle  12980  ioo0  13423  ico0  13444  ioc0  13445  icc0  13446  fzen  13595  modcyc  13967  expgt0  14159  expge0  14162  expge1  14163  swrdrevpfx  14838  2cshwcom  14887  shftval2  15148  abs3dif  15419  divalgb  16494  submrc  17716  mrieqv2d  17727  pltnlt  18426  pltn2lp  18427  tosso  18505  latnle  18561  latabs1  18563  lubel  18602  ipopos  18624  grpinvcnv  19130  mulgaddcom  19221  mulgneg2  19231  oppgmnd  19481  oddvdsnn0  19671  oddvds  19674  odmulg  19683  odcl2  19692  lsmcomx  19983  srgcom4  20353  srgrmhm  20361  ringcom  20421  mulgass2  20451  opprrng  20486  irredrmul  20568  irredlmul  20569  isdrngrd  20932  isdrngrdOLD  20934  islmodd  21050  lmodcom  21092  rmodislmod  21114  zntoslem  21769  ipcl  21846  evls1fpws  22594  maducoevalmin1  22874  rintopn  23134  opnnei  23345  restin  23391  cnpnei  23489  cnprest  23514  ordthaus  23609  kgen2ss  23781  hausflim  24207  fclsfnflim  24253  cnpfcf  24267  opnsubg  24334  cuspcvg  24526  psmetsym  24536  xmetsym  24573  ngpdsr  24831  ngpds2r  24833  ngpds3r  24835  clmmulg  25329  cphipval2  25469  iscau2  25505  dgr1term  26486  cxpeq0  26915  cxpge0  26920  relogbzcl  27011  negsunif  28320  oldfib  28642  grpoidinvlem2  30986  grpoinvdiv  31018  nvpncan  31135  nvabs  31153  ipval2lem2  31185  dipcj  31195  diporthcom  31197  dipdi  31324  dipassr  31327  dipsubdi  31330  hlipcj  31392  hvadd32  31515  hvsub32  31526  his5  31567  hoadd32  32264  hosubsub  32298  unopf1o  32397  adj2  32415  adjvalval  32418  adjlnop  32567  leopmul2i  32616  cvntr  32773  mdsymlem5  32888  sumdmdii  32896  supxrnemnf  33239  odutos  33408  tlt2  33409  tosglblem  33414  archiabl  33638  unitdivcld  34411  bnj605  35416  bnj607  35425  rankfilimb  35610  r1filim  35612  fisshasheq  35717  cusgredgex  35720  acycgr1v  35728  gcd32  36328  cgrrflx  36567  cgrcom  36570  cgrcomr  36577  btwntriv1  36596  cgr3com  36633  colineartriv2  36648  segleantisym  36695  seglelin  36696  btwnoutside  36705  clsint2  36948  dissneqlem  38094  ftc1anclem5  38446  heibor1  38560  rngoidl  38774  ispridlc  38820  opltcon3b  40077  cmtcomlemN  40121  cmtcomN  40122  cmt3N  40124  cmtbr3N  40127  cvrval2  40147  cvrnbtwn4  40152  leatb  40165  atlrelat1  40194  hlatlej2  40249  hlateq  40272  hlrelat5N  40274  snatpsubN  40623  pmap11  40635  paddcom  40686  sspadd2  40689  paddss12  40692  cdleme51finvN  41429  cdleme51finvtrN  41431  cdlemeiota  41458  cdlemg2jlemOLDN  41466  cdlemg2klem  41468  cdlemg4b1  41482  cdlemg4b2  41483  trljco2  41614  tgrpabl  41624  tendoplcom  41655  cdleml6  41854  erngdvlem3-rN  41871  dia11N  41921  dib11N  42033  dih11  42138  uzindd  42844  lcmineqlem1  42895  nerabdioph  43650  monotoddzzfi  43783  fzneg  43823  jm2.19lem2  43831  ismnushort  45125  nzss  45141  sineq0ALT  45759  lincvalsng  49346  reccot  50684