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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3coml  1128  3anidm13  1421  eqreu  3726  f1ofveu  7403  curry2f  8094  dfsmo2  8347  nneob  8655  nadd32  8696  f1oeng  8967  domnsymfi  9203  sdomdomtrfi  9204  domsdomtrfi  9205  php  9210  php3  9212  suppr  9466  infdif  10204  axdclem2  10515  gchen1  10620  grumap  10803  grudomon  10812  mul32  11380  add32  11432  subsub23  11465  subadd23  11472  addsub12  11473  subsub  11490  subsub3  11492  sub32  11494  suble  11692  lesub  11693  ltsub23  11694  ltsub13  11695  ltleadd  11697  div32  11892  div13  11893  div12  11894  divdiv32  11922  cju  12208  infssuzle  12915  ioo0  13349  ico0  13370  ioc0  13371  icc0  13372  fzen  13518  modcyc  13871  expgt0  14061  expge0  14064  expge1  14065  2cshwcom  14766  shftval2  15022  abs3dif  15278  divalgb  16347  submrc  17572  mrieqv2d  17583  pltnlt  18293  pltn2lp  18294  tosso  18372  latnle  18426  latabs1  18428  lubel  18467  ipopos  18489  grpinvcnv  18891  mulgaddcom  18978  mulgneg2  18988  oppgmnd  19221  oddvdsnn0  19412  oddvds  19415  odmulg  19424  odcl2  19433  lsmcomx  19724  srgcom4  20037  srgrmhm  20045  ringcom  20097  mulgass2  20121  opprring  20161  irredrmul  20241  irredlmul  20242  isdrngrd  20391  isdrngrdOLD  20393  islmodd  20477  lmodcom  20518  rmodislmod  20540  rmodislmodOLD  20541  opprdomn  20919  zntoslem  21112  ipcl  21186  maducoevalmin1  22154  rintopn  22411  opnnei  22624  restin  22670  cnpnei  22768  cnprest  22793  ordthaus  22888  kgen2ss  23059  hausflim  23485  fclsfnflim  23531  cnpfcf  23545  opnsubg  23612  cuspcvg  23806  psmetsym  23816  xmetsym  23853  ngpdsr  24114  ngpds2r  24116  ngpds3r  24118  clmmulg  24617  cphipval2  24758  iscau2  24794  dgr1term  25774  cxpeq0  26186  cxpge0  26191  relogbzcl  26279  negsunif  27529  grpoidinvlem2  29758  grpoinvdiv  29790  nvpncan  29907  nvabs  29925  ipval2lem2  29957  dipcj  29967  diporthcom  29969  dipdi  30096  dipassr  30099  dipsubdi  30102  hlipcj  30164  hvadd32  30287  hvsub32  30298  his5  30339  hoadd32  31036  hosubsub  31070  unopf1o  31169  adj2  31187  adjvalval  31190  adjlnop  31339  leopmul2i  31388  cvntr  31545  mdsymlem5  31660  sumdmdii  31668  supxrnemnf  31981  odutos  32138  tlt2  32139  tosglblem  32144  archiabl  32344  evls1fpws  32646  unitdivcld  32881  bnj605  33918  bnj607  33927  fisshasheq  34104  swrdrevpfx  34107  cusgredgex  34112  acycgr1v  34140  gcd32  34719  cgrrflx  34959  cgrcom  34962  cgrcomr  34969  btwntriv1  34988  cgr3com  35025  colineartriv2  35040  segleantisym  35087  seglelin  35088  btwnoutside  35097  clsint2  35214  dissneqlem  36221  ftc1anclem5  36565  heibor1  36678  rngoidl  36892  ispridlc  36938  opltcon3b  38074  cmtcomlemN  38118  cmtcomN  38119  cmt3N  38121  cmtbr3N  38124  cvrval2  38144  cvrnbtwn4  38149  leatb  38162  atlrelat1  38191  hlatlej2  38246  hlateq  38270  hlrelat5N  38272  snatpsubN  38621  pmap11  38633  paddcom  38684  sspadd2  38687  paddss12  38690  cdleme51finvN  39427  cdleme51finvtrN  39429  cdlemeiota  39456  cdlemg2jlemOLDN  39464  cdlemg2klem  39466  cdlemg4b1  39480  cdlemg4b2  39481  trljco2  39612  tgrpabl  39622  tendoplcom  39653  cdleml6  39852  erngdvlem3-rN  39869  dia11N  39919  dib11N  40031  dih11  40136  uzindd  40842  lcmineqlem1  40894  nerabdioph  41547  monotoddzzfi  41681  fzneg  41721  jm2.19lem2  41729  ismnushort  43060  nzss  43076  sineq0ALT  43698  opprrng  46674  lincvalsng  47097  reccot  47803