Theorem 3com23 1160

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

Syntax hints:   → wi 4   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  3coml  1161  syld3an2OLD  1536  3anidm13  1547  eqreu  3623  f1ofveu  6900  curry2f  7537  dfsmo2  7710  nneob  7999  f1oeng  8241  suppr  8646  infdif  9346  axdclem2  9657  gchen1  9762  grumap  9945  grudomon  9954  mul32  10522  add32  10573  subsub23  10606  subadd23  10614  addsub12  10615  subsub  10632  subsub3  10634  sub32  10636  suble  10830  lesub  10831  ltsub23  10832  ltsub13  10833  ltleadd  10835  div32  11030  div13  11031  div12  11032  divdiv32  11059  cju  11346  infssuzle  12054  ioo0  12488  ico0  12509  ioc0  12510  icc0  12511  fzen  12651  modcyc  13000  expgt0  13187  expge0  13190  expge1  13191  2cshwcom  13937  shftval2  14192  abs3dif  14448  divalgb  15501  submrc  16641  mrieqv2d  16652  pltnlt  17321  pltn2lp  17322  tosso  17389  latnle  17438  latabs1  17440  lubel  17475  ipopos  17513  grpinvcnv  17837  mulgneg2  17927  oppgmnd  18134  oddvdsnn0  18314  oddvds  18317  odmulg  18324  odcl2  18333  lsmcomx  18612  srgrmhm  18890  ringcom  18933  mulgass2  18955  opprring  18985  irredrmul  19061  irredlmul  19062  isdrngrd  19129  islmodd  19225  lmodcom  19265  rmodislmod  19287  opprdomn  19662  zntoslem  20264  ipcl  20340  maducoevalmin1  20827  rintopn  21084  opnnei  21295  restin  21341  cnpnei  21439  cnprest  21464  ordthaus  21559  kgen2ss  21729  hausflim  22155  fclsfnflim  22201  cnpfcf  22215  opnsubg  22281  cuspcvg  22475  psmetsym  22485  xmetsym  22522  ngpdsr  22779  ngpds2r  22781  ngpds3r  22783  clmmulg  23270  cphipval2  23409  iscau2  23445  dgr1term  24415  cxpeq0  24823  cxpge0  24828  relogbzcl  24914  grpoidinvlem2  27904  grpoinvdiv  27936  nvpncan  28053  nvabs  28071  ipval2lem2  28103  dipcj  28113  diporthcom  28115  dipdi  28242  dipassr  28245  dipsubdi  28248  hlipcj  28311  hvadd32  28435  hvsub32  28446  his5  28487  hoadd32  29186  hosubsub  29220  unopf1o  29319  adj2  29337  adjvalval  29340  adjlnop  29489  leopmul2i  29538  cvntr  29695  mdsymlem5  29810  sumdmdii  29818  supxrnemnf  30070  odutos  30197  tlt2  30198  tosglblem  30203  archiabl  30286  unitdivcld  30481  bnj605  31512  bnj607  31521  gcd32  32168  cgrrflx  32622  cgrcom  32625  cgrcomr  32632  btwntriv1  32651  cgr3com  32688  colineartriv2  32703  segleantisym  32750  seglelin  32751  btwnoutside  32760  clsint2  32851  dissneqlem  33726  ftc1anclem5  34025  heibor1  34144  rngoidl  34358  ispridlc  34404  opltcon3b  35272  cmtcomlemN  35316  cmtcomN  35317  cmt3N  35319  cmtbr3N  35322  cvrval2  35342  cvrnbtwn4  35347  leatb  35360  atlrelat1  35389  hlatlej2  35444  hlateq  35467  hlrelat5N  35469  snatpsubN  35818  pmap11  35830  paddcom  35881  sspadd2  35884  paddss12  35887  cdleme51finvN  36624  cdleme51finvtrN  36626  cdlemeiota  36653  cdlemg2jlemOLDN  36661  cdlemg2klem  36663  cdlemg4b1  36677  cdlemg4b2  36678  trljco2  36809  tgrpabl  36819  tendoplcom  36850  cdleml6  37049  erngdvlem3-rN  37066  dia11N  37116  dib11N  37228  dih11  37333  nerabdioph  38210  monotoddzzfi  38343  fzneg  38385  jm2.19lem2  38393  nzss  39349  sineq0ALT  39984  lincvalsng  43045  reccot  43390