Theorem 3com23 1156

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

Syntax hints:   → wi 4   ∧ w3a 1107

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 198  df-an 385  df-3an 1109

This theorem is referenced by:  3coml  1157  syld3an2OLD  1532  3anidm13  1543  eqreu  3559  f1ofveu  6841  curry2f  7479  dfsmo2  7652  nneob  7941  f1oeng  8183  suppr  8588  infdif  9288  axdclem2  9599  gchen1  9704  grumap  9887  grudomon  9896  mul32  10461  add32  10512  subsub23  10544  subadd23  10551  addsub12  10552  subsub  10569  subsub3  10571  sub32  10573  suble  10764  lesub  10765  ltsub23  10766  ltsub13  10767  ltleadd  10769  div32  10963  div13  10964  div12  10965  divdiv32  10991  cju  11274  infssuzle  11977  ioo0  12407  ico0  12428  ioc0  12429  icc0  12430  fzen  12570  modcyc  12918  expgt0  13105  expge0  13108  expge1  13109  2cshwcom  13859  shftval2  14114  abs3dif  14370  divalgb  15423  submrc  16568  mrieqv2d  16579  pltnlt  17248  pltn2lp  17249  tosso  17316  latnle  17365  latabs1  17367  lubel  17402  ipopos  17440  grpinvcnv  17764  mulgneg2  17854  oppgmnd  18061  oddvdsnn0  18241  oddvds  18244  odmulg  18251  odcl2  18260  lsmcomx  18539  srgrmhm  18817  ringcom  18860  mulgass2  18882  opprring  18912  irredrmul  18988  irredlmul  18989  isdrngrd  19056  islmodd  19152  lmodcom  19192  rmodislmod  19214  opprdomn  19589  zntoslem  20191  ipcl  20267  maducoevalmin1  20750  rintopn  21007  opnnei  21218  restin  21264  cnpnei  21362  cnprest  21387  ordthaus  21482  kgen2ss  21652  hausflim  22078  fclsfnflim  22124  cnpfcf  22138  opnsubg  22204  cuspcvg  22398  psmetsym  22408  xmetsym  22445  ngpdsr  22702  ngpds2r  22704  ngpds3r  22706  clmmulg  23193  cphipval2  23332  iscau2  23368  dgr1term  24321  cxpeq0  24729  cxpge0  24734  relogbzcl  24817  grpoidinvlem2  27837  grpoinvdiv  27869  nvpncan  27986  nvabs  28004  ipval2lem2  28036  dipcj  28046  diporthcom  28048  dipdi  28175  dipassr  28178  dipsubdi  28181  hlipcj  28244  hvadd32  28368  hvsub32  28379  his5  28420  hoadd32  29119  hosubsub  29153  unopf1o  29252  adj2  29270  adjvalval  29273  adjlnop  29422  leopmul2i  29471  cvntr  29628  mdsymlem5  29743  sumdmdii  29751  supxrnemnf  30004  odutos  30131  tlt2  30132  tosglblem  30137  archiabl  30220  unitdivcld  30415  bnj605  31446  bnj607  31455  gcd32  32103  cgrrflx  32559  cgrcom  32562  cgrcomr  32569  btwntriv1  32588  cgr3com  32625  colineartriv2  32640  segleantisym  32687  seglelin  32688  btwnoutside  32697  clsint2  32788  dissneqlem  33642  ftc1anclem5  33933  heibor1  34052  rngoidl  34266  ispridlc  34312  opltcon3b  35181  cmtcomlemN  35225  cmtcomN  35226  cmt3N  35228  cmtbr3N  35231  cvrval2  35251  cvrnbtwn4  35256  leatb  35269  atlrelat1  35298  hlatlej2  35353  hlateq  35376  hlrelat5N  35378  snatpsubN  35727  pmap11  35739  paddcom  35790  sspadd2  35793  paddss12  35796  cdleme51finvN  36533  cdleme51finvtrN  36535  cdlemeiota  36562  cdlemg2jlemOLDN  36570  cdlemg2klem  36572  cdlemg4b1  36586  cdlemg4b2  36587  trljco2  36718  tgrpabl  36728  tendoplcom  36759  cdleml6  36958  erngdvlem3-rN  36975  dia11N  37025  dib11N  37137  dih11  37242  nerabdioph  38075  monotoddzzfi  38208  fzneg  38250  jm2.19lem2  38258  nzss  39214  sineq0ALT  39849  lincvalsng  42898  reccot  43195