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  7412  curry2f  8117  dfsmo2  8348  nneob  8658  nadd32  8700  f1oeng  8990  domnsymfi  9208  sdomdomtrfi  9209  domsdomtrfi  9210  php  9215  php3  9217  fodomfir  9312  suppr  9457  infdif  10279  axdclem2  10591  gchen1  10703  grumap  10886  grudomon  10895  mul32  11469  add32  11522  subsub23  11555  subadd23  11562  addsub12  11563  subsub  11581  subsub3  11583  sub32  11585  suble  11787  lesub  11788  ltsub23  11789  ltsub13  11790  ltleadd  11792  div32  11987  div13  11988  div12  11989  divdiv32  12018  cju  12309  infssuzle  13051  ioo0  13494  ico0  13515  ioc0  13516  icc0  13517  fzen  13667  modcyc  14039  expgt0  14231  expge0  14234  expge1  14235  swrdrevpfx  14911  2cshwcom  14960  shftval2  15221  abs3dif  15492  divalgb  16567  submrc  17795  mrieqv2d  17806  pltnlt  18505  pltn2lp  18506  tosso  18584  latnle  18640  latabs1  18642  lubel  18681  ipopos  18703  grpinvcnv  19210  mulgaddcom  19301  mulgneg2  19311  oppgmnd  19561  oddvdsnn0  19751  oddvds  19754  odmulg  19763  odcl2  19772  lsmcomx  20063  srgcom4  20433  srgrmhm  20441  ringcom  20502  mulgass2  20533  opprrng  20568  irredrmul  20650  irredlmul  20651  isdrngrd  21016  isdrngrdOLD  21018  islmodd  21134  lmodcom  21176  rmodislmod  21198  zntoslem  21855  ipcl  21932  evls1fpws  22680  maducoevalmin1  22960  rintopn  23220  opnnei  23431  restin  23477  cnpnei  23575  cnprest  23600  ordthaus  23695  kgen2ss  23867  hausflim  24293  fclsfnflim  24339  cnpfcf  24353  opnsubg  24420  cuspcvg  24612  psmetsym  24622  xmetsym  24659  ngpdsr  24917  ngpds2r  24919  ngpds3r  24921  clmmulg  25415  cphipval2  25555  iscau2  25591  dgr1term  26572  cxpeq0  26999  cxpge0  27004  relogbzcl  27095  negsunif  28434  oldfib  28756  grpoidinvlem2  31100  grpoinvdiv  31132  nvpncan  31249  nvabs  31267  ipval2lem2  31299  dipcj  31309  diporthcom  31311  dipdi  31438  dipassr  31441  dipsubdi  31444  hlipcj  31506  hvadd32  31629  hvsub32  31640  his5  31681  hoadd32  32378  hosubsub  32412  unopf1o  32511  adj2  32529  adjvalval  32532  adjlnop  32681  leopmul2i  32730  cvntr  32887  mdsymlem5  33002  sumdmdii  33010  supxrnemnf  33353  odutos  33522  tlt2  33523  tosglblem  33528  archiabl  33752  unitdivcld  34526  bnj605  35530  bnj607  35539  rankfilimb  35717  r1filim  35718  fisshasheq  35882  cusgredgex  35885  acycgr1v  35893  gcd32  36493  cgrrflx  36732  cgrcom  36735  cgrcomr  36742  btwntriv1  36761  cgr3com  36798  colineartriv2  36813  segleantisym  36860  seglelin  36861  btwnoutside  36870  clsint2  37097  dissneqlem  38243  ftc1anclem5  38595  heibor1  38724  rngoidl  38938  ispridlc  38984  opltcon3b  40241  cmtcomlemN  40285  cmtcomN  40286  cmt3N  40288  cmtbr3N  40291  cvrval2  40311  cvrnbtwn4  40316  leatb  40329  atlrelat1  40358  hlatlej2  40413  hlateq  40436  hlrelat5N  40438  snatpsubN  40787  pmap11  40799  paddcom  40850  sspadd2  40853  paddss12  40856  cdleme51finvN  41593  cdleme51finvtrN  41595  cdlemeiota  41622  cdlemg2jlemOLDN  41630  cdlemg2klem  41632  cdlemg4b1  41646  cdlemg4b2  41647  trljco2  41778  tgrpabl  41788  tendoplcom  41819  cdleml6  42018  erngdvlem3-rN  42035  dia11N  42085  dib11N  42197  dih11  42302  uzindd  43008  lcmineqlem1  43059  nerabdioph  43795  monotoddzzfi  43928  fzneg  43968  jm2.19lem2  43976  ismnushort  45270  nzss  45286  sineq0ALT  45904  lincvalsng  49497  reccot  50820