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  3686  f1ofveu  7416  curry2f  8123  dfsmo2  8360  nneob  8670  nadd32  8712  f1oeng  9002  domnsymfi  9220  sdomdomtrfi  9221  domsdomtrfi  9222  php  9227  php3  9229  fodomfir  9324  suppr  9469  infdif  10291  axdclem2  10603  gchen1  10715  grumap  10898  grudomon  10907  mul32  11481  add32  11534  subsub23  11567  subadd23  11574  addsub12  11575  subsub  11593  subsub3  11595  sub32  11597  suble  11799  lesub  11800  ltsub23  11801  ltsub13  11802  ltleadd  11804  div32  11999  div13  12000  div12  12001  divdiv32  12030  cju  12321  infssuzle  13063  ioo0  13506  ico0  13527  ioc0  13528  icc0  13529  fzen  13679  modcyc  14051  expgt0  14243  expge0  14246  expge1  14247  swrdrevpfx  14924  2cshwcom  14973  shftval2  15235  abs3dif  15506  divalgb  16581  submrc  17809  mrieqv2d  17820  pltnlt  18519  pltn2lp  18520  tosso  18598  latnle  18654  latabs1  18656  lubel  18695  ipopos  18717  grpinvcnv  19224  mulgaddcom  19315  mulgneg2  19325  oppgmnd  19575  oddvdsnn0  19765  oddvds  19768  odmulg  19777  odcl2  19786  lsmcomx  20077  srgcom4  20447  srgrmhm  20455  ringcom  20516  mulgass2  20547  opprrng  20582  irredrmul  20664  irredlmul  20665  isdrngrd  21030  isdrngrdOLD  21032  islmodd  21148  lmodcom  21190  rmodislmod  21212  zntoslem  21869  ipcl  21946  evls1fpws  22694  maducoevalmin1  22974  rintopn  23234  opnnei  23445  restin  23491  cnpnei  23589  cnprest  23614  ordthaus  23709  kgen2ss  23881  hausflim  24307  fclsfnflim  24353  cnpfcf  24367  opnsubg  24434  cuspcvg  24626  psmetsym  24636  xmetsym  24673  ngpdsr  24931  ngpds2r  24933  ngpds3r  24935  clmmulg  25429  cphipval2  25569  iscau2  25605  dgr1term  26586  cxpeq0  27013  cxpge0  27018  relogbzcl  27109  negsunif  28448  oldfib  28770  grpoidinvlem2  31114  grpoinvdiv  31146  nvpncan  31263  nvabs  31281  ipval2lem2  31313  dipcj  31323  diporthcom  31325  dipdi  31452  dipassr  31455  dipsubdi  31458  hlipcj  31520  hvadd32  31643  hvsub32  31654  his5  31695  hoadd32  32392  hosubsub  32426  unopf1o  32525  adj2  32543  adjvalval  32546  adjlnop  32695  leopmul2i  32744  cvntr  32901  mdsymlem5  33016  sumdmdii  33024  supxrnemnf  33408  odutos  33577  tlt2  33578  tosglblem  33583  archiabl  33807  unitdivcld  34581  bnj605  35585  bnj607  35594  rankfilimb  35782  r1filim  35783  fisshasheq  35981  cusgredgex  35984  acycgr1v  35992  gcd32  36608  cgrrflx  36846  cgrcom  36849  cgrcomr  36856  btwntriv1  36875  cgr3com  36912  colineartriv2  36927  segleantisym  36974  seglelin  36975  btwnoutside  36984  clsint2  37211  dissneqlem  38370  ftc1anclem5  38722  heibor1  38851  rngoidl  39065  ispridlc  39111  opltcon3b  40368  cmtcomlemN  40412  cmtcomN  40413  cmt3N  40415  cmtbr3N  40418  cvrval2  40438  cvrnbtwn4  40443  leatb  40456  atlrelat1  40485  hlatlej2  40540  hlateq  40563  hlrelat5N  40565  snatpsubN  40914  pmap11  40926  paddcom  40977  sspadd2  40980  paddss12  40983  cdleme51finvN  41720  cdleme51finvtrN  41722  cdlemeiota  41749  cdlemg2jlemOLDN  41757  cdlemg2klem  41759  cdlemg4b1  41773  cdlemg4b2  41774  trljco2  41905  tgrpabl  41915  tendoplcom  41946  cdleml6  42145  erngdvlem3-rN  42162  dia11N  42212  dib11N  42324  dih11  42429  uzindd  43135  lcmineqlem1  43186  nerabdioph  43923  monotoddzzfi  44056  fzneg  44096  jm2.19lem2  44104  ismnushort  45392  nzss  45408  sineq0ALT  46026  lincvalsng  49635  reccot  51033