Theorem 3com23 1127

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3coml  1128  3anidm13  1423  eqreu  3689  f1ofveu  7362  curry2f  8060  dfsmo2  8289  nneob  8594  nadd32  8635  f1oeng  8919  domnsymfi  9136  sdomdomtrfi  9137  domsdomtrfi  9138  php  9143  php3  9145  fodomfir  9240  suppr  9387  infdif  10130  axdclem2  10442  gchen1  10548  grumap  10731  grudomon  10740  mul32  11311  add32  11364  subsub23  11397  subadd23  11404  addsub12  11405  subsub  11423  subsub3  11425  sub32  11427  suble  11627  lesub  11628  ltsub23  11629  ltsub13  11630  ltleadd  11632  div32  11828  div13  11829  div12  11830  divdiv32  11861  cju  12153  infssuzle  12856  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  fzen  13469  modcyc  13838  expgt0  14030  expge0  14033  expge1  14034  2cshwcom  14751  shftval2  15010  abs3dif  15267  divalgb  16343  submrc  17563  mrieqv2d  17574  pltnlt  18273  pltn2lp  18274  tosso  18352  latnle  18408  latabs1  18410  lubel  18449  ipopos  18471  grpinvcnv  18948  mulgaddcom  19040  mulgneg2  19050  oppgmnd  19295  oddvdsnn0  19485  oddvds  19488  odmulg  19497  odcl2  19506  lsmcomx  19797  srgcom4  20161  srgrmhm  20169  ringcom  20227  mulgass2  20256  opprrng  20293  irredrmul  20375  irredlmul  20376  isdrngrd  20711  isdrngrdOLD  20713  islmodd  20829  lmodcom  20871  rmodislmod  20893  zntoslem  21523  ipcl  21600  evls1fpws  22325  maducoevalmin1  22608  rintopn  22865  opnnei  23076  restin  23122  cnpnei  23220  cnprest  23245  ordthaus  23340  kgen2ss  23511  hausflim  23937  fclsfnflim  23983  cnpfcf  23997  opnsubg  24064  cuspcvg  24256  psmetsym  24266  xmetsym  24303  ngpdsr  24561  ngpds2r  24563  ngpds3r  24565  clmmulg  25069  cphipval2  25209  iscau2  25245  dgr1term  26233  cxpeq0  26655  cxpge0  26660  relogbzcl  26752  negsunif  28063  oldfib  28385  grpoidinvlem2  30593  grpoinvdiv  30625  nvpncan  30742  nvabs  30760  ipval2lem2  30792  dipcj  30802  diporthcom  30804  dipdi  30931  dipassr  30934  dipsubdi  30937  hlipcj  30999  hvadd32  31122  hvsub32  31133  his5  31174  hoadd32  31871  hosubsub  31905  unopf1o  32004  adj2  32022  adjvalval  32025  adjlnop  32174  leopmul2i  32223  cvntr  32380  mdsymlem5  32495  sumdmdii  32503  supxrnemnf  32859  odutos  33061  tlt2  33062  tosglblem  33067  archiabl  33292  unitdivcld  34079  bnj605  35083  bnj607  35092  rankfilimb  35279  r1filim  35281  fisshasheq  35331  swrdrevpfx  35333  cusgredgex  35338  acycgr1v  35365  gcd32  35965  cgrrflx  36203  cgrcom  36206  cgrcomr  36213  btwntriv1  36232  cgr3com  36269  colineartriv2  36284  segleantisym  36331  seglelin  36332  btwnoutside  36341  clsint2  36545  dissneqlem  37595  ftc1anclem5  37948  heibor1  38061  rngoidl  38275  ispridlc  38321  opltcon3b  39580  cmtcomlemN  39624  cmtcomN  39625  cmt3N  39627  cmtbr3N  39630  cvrval2  39650  cvrnbtwn4  39655  leatb  39668  atlrelat1  39697  hlatlej2  39752  hlateq  39775  hlrelat5N  39777  snatpsubN  40126  pmap11  40138  paddcom  40189  sspadd2  40192  paddss12  40195  cdleme51finvN  40932  cdleme51finvtrN  40934  cdlemeiota  40961  cdlemg2jlemOLDN  40969  cdlemg2klem  40971  cdlemg4b1  40985  cdlemg4b2  40986  trljco2  41117  tgrpabl  41127  tendoplcom  41158  cdleml6  41357  erngdvlem3-rN  41374  dia11N  41424  dib11N  41536  dih11  41641  uzindd  42347  lcmineqlem1  42399  nerabdioph  43166  monotoddzzfi  43299  fzneg  43339  jm2.19lem2  43347  ismnushort  44657  nzss  44673  sineq0ALT  45292  lincvalsng  48776  reccot  50117