Theorem 3com23 1291

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

Syntax hints:   → wi 4   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3coml  1292  syld3an2  1413  3anidm13  1424  eqreu  3431  f1ofveu  6685  curry2f  7318  dfsmo2  7489  nneob  7777  f1oeng  8016  suppr  8418  infdif  9069  axdclem2  9380  gchen1  9485  grumap  9668  grudomon  9677  mul32  10241  add32  10292  subsub23  10324  subadd23  10331  addsub12  10332  subsub  10349  subsub3  10351  sub32  10353  suble  10544  lesub  10545  ltsub23  10546  ltsub13  10547  ltleadd  10549  div32  10743  div13  10744  div12  10745  divdiv32  10771  cju  11054  infssuzle  11809  ioo0  12238  ico0  12259  ioc0  12260  icc0  12261  fzen  12396  modcyc  12745  expgt0  12933  expge0  12936  expge1  12937  2cshwcom  13608  shftval2  13859  abs3dif  14115  divalgb  15174  submrc  16335  mrieqv2d  16346  pltnlt  17015  pltn2lp  17016  tosso  17083  latnle  17132  latabs1  17134  lubel  17169  ipopos  17207  grpinvcnv  17530  mulgneg2  17622  oppgmnd  17830  oddvdsnn0  18009  oddvds  18012  odmulg  18019  odcl2  18028  lsmcomx  18305  srgrmhm  18582  ringcom  18625  mulgass2  18647  opprring  18677  irredrmul  18753  irredlmul  18754  isdrngrd  18821  islmodd  18917  lmodcom  18957  rmodislmod  18979  opprdomn  19349  zntoslem  19953  ipcl  20026  maducoevalmin1  20506  rintopn  20762  opnnei  20972  restin  21018  cnpnei  21116  cnprest  21141  ordthaus  21236  kgen2ss  21406  hausflim  21832  fclsfnflim  21878  cnpfcf  21892  opnsubg  21958  cuspcvg  22152  psmetsym  22162  xmetsym  22199  ngpdsr  22456  ngpds2r  22458  ngpds3r  22460  clmmulg  22947  cphipval2  23086  iscau2  23121  dgr1term  24061  cxpeq0  24469  cxpge0  24474  relogbzcl  24557  grpoidinvlem2  27487  grpoinvdiv  27519  nvpncan  27637  nvabs  27655  ipval2lem2  27687  dipcj  27697  diporthcom  27699  dipdi  27826  dipassr  27829  dipsubdi  27832  hlipcj  27895  hvadd32  28019  hvsub32  28030  his5  28071  hoadd32  28770  hosubsub  28804  unopf1o  28903  adj2  28921  adjvalval  28924  adjlnop  29073  leopmul2i  29122  cvntr  29279  mdsymlem5  29394  sumdmdii  29402  supxrnemnf  29662  odutos  29791  tlt2  29792  tosglblem  29797  archiabl  29880  unitdivcld  30075  bnj605  31103  bnj607  31112  gcd32  31763  cgrrflx  32219  cgrcom  32222  cgrcomr  32229  btwntriv1  32248  cgr3com  32285  colineartriv2  32300  segleantisym  32347  seglelin  32348  btwnoutside  32357  clsint2  32449  dissneqlem  33317  ftc1anclem5  33619  heibor1  33739  rngoidl  33953  ispridlc  33999  opltcon3b  34809  cmtcomlemN  34853  cmtcomN  34854  cmt3N  34856  cmtbr3N  34859  cvrval2  34879  cvrnbtwn4  34884  leatb  34897  atlrelat1  34926  hlatlej2  34980  hlateq  35003  hlrelat5N  35005  snatpsubN  35354  pmap11  35366  paddcom  35417  sspadd2  35420  paddss12  35423  cdleme51finvN  36161  cdleme51finvtrN  36163  cdlemeiota  36190  cdlemg2jlemOLDN  36198  cdlemg2klem  36200  cdlemg4b1  36214  cdlemg4b2  36215  trljco2  36346  tgrpabl  36356  tendoplcom  36387  cdleml6  36586  erngdvlem3-rN  36603  dia11N  36654  dib11N  36766  dih11  36871  nerabdioph  37690  monotoddzzfi  37824  fzneg  37866  jm2.19lem2  37874  nzss  38833  sineq0ALT  39487  lincvalsng  42530  reccot  42827