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  1448  eqreu  3690  f1ofveu  7445  curry2f  8156  dfsmo2  8393  nneob  8703  nadd32  8745  f1oeng  9035  domnsymfi  9253  sdomdomtrfi  9254  domsdomtrfi  9255  php  9260  php3  9262  fodomfir  9357  suppr  9501  infdif  10325  axdclem2  10637  gchen1  10749  grumap  10932  grudomon  10941  mul32  11515  add32  11568  subsub23  11601  subadd23  11608  addsub12  11609  subsub  11627  subsub3  11629  sub32  11631  suble  11834  lesub  11835  ltsub23  11836  ltsub13  11837  ltleadd  11839  div32  12034  div13  12035  div12  12036  divdiv32  12065  cju  12356  infssuzle  13098  ioo0  13541  ico0  13562  ioc0  13563  icc0  13564  fzen  13714  modcyc  14086  expgt0  14278  expge0  14281  expge1  14282  swrdrevpfx  14960  2cshwcom  15009  shftval2  15271  abs3dif  15542  divalgb  16618  submrc  17852  mrieqv2d  17863  pltnlt  18562  pltn2lp  18563  tosso  18641  latnle  18697  latabs1  18699  lubel  18738  ipopos  18760  grpinvcnv  19267  mulgaddcom  19358  mulgneg2  19368  oppgmnd  19619  oddvdsnn0  19809  oddvds  19812  odmulg  19821  odcl2  19830  lsmcomx  20121  srgcom4  20491  srgrmhm  20499  ringcom  20560  mulgass2  20591  opprrng  20626  irredrmul  20708  irredlmul  20709  isdrngrd  21074  isdrngrdOLD  21076  islmodd  21192  lmodcom  21234  rmodislmod  21256  zntoslem  21917  ipcl  21994  evls1fpws  22742  maducoevalmin1  23022  rintopn  23282  opnnei  23493  restin  23539  cnpnei  23637  cnprest  23662  ordthaus  23757  kgen2ss  23929  hausflim  24355  fclsfnflim  24401  cnpfcf  24415  opnsubg  24482  cuspcvg  24674  psmetsym  24684  xmetsym  24721  ngpdsr  24979  ngpds2r  24981  ngpds3r  24983  clmmulg  25477  cphipval2  25617  iscau2  25653  dgr1term  26634  cxpeq0  27063  cxpge0  27068  relogbzcl  27159  negsunif  28498  oldfib  28820  grpoidinvlem2  31164  grpoinvdiv  31196  nvpncan  31313  nvabs  31331  ipval2lem2  31363  dipcj  31373  diporthcom  31375  dipdi  31502  dipassr  31505  dipsubdi  31508  hlipcj  31570  hvadd32  31693  hvsub32  31704  his5  31745  hoadd32  32442  hosubsub  32476  unopf1o  32575  adj2  32593  adjvalval  32596  adjlnop  32745  leopmul2i  32794  cvntr  32951  mdsymlem5  33066  sumdmdii  33074  supxrnemnf  33456  odutos  33625  tlt2  33626  tosglblem  33631  archiabl  33858  unitdivcld  34644  bnj605  35648  bnj607  35657  rankfilimb  35853  r1filim  35854  fisshasheq  36101  cusgredgex  36104  acycgr1v  36112  gcd32  36729  cgrrflx  36967  cgrcom  36970  cgrcomr  36977  btwntriv1  36996  cgr3com  37033  colineartriv2  37048  segleantisym  37095  seglelin  37096  btwnoutside  37105  clsint2  37332  dissneqlem  38531  ftc1anclem5  38883  heibor1  39010  rngoidl  39224  ispridlc  39270  opltcon3b  40527  cmtcomlemN  40571  cmtcomN  40572  cmt3N  40574  cmtbr3N  40577  cvrval2  40597  cvrnbtwn4  40602  leatb  40615  atlrelat1  40644  hlatlej2  40699  hlateq  40722  hlrelat5N  40724  snatpsubN  41073  pmap11  41085  paddcom  41136  sspadd2  41139  paddss12  41142  cdleme51finvN  41879  cdleme51finvtrN  41881  cdlemeiota  41908  cdlemg2jlemOLDN  41916  cdlemg2klem  41918  cdlemg4b1  41932  cdlemg4b2  41933  trljco2  42064  tgrpabl  42074  tendoplcom  42105  cdleml6  42304  erngdvlem3-rN  42321  dia11N  42371  dib11N  42483  dih11  42588  uzindd  43294  lcmineqlem1  43345  nerabdioph  44082  monotoddzzfi  44215  fzneg  44255  jm2.19lem2  44263  ismnushort  45546  nzss  45562  sineq0ALT  46179  lincvalsng  49859  reccot  51279