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  27532  grpoidinvlem2  29789  grpoinvdiv  29821  nvpncan  29938  nvabs  29956  ipval2lem2  29988  dipcj  29998  diporthcom  30000  dipdi  30127  dipassr  30130  dipsubdi  30133  hlipcj  30195  hvadd32  30318  hvsub32  30329  his5  30370  hoadd32  31067  hosubsub  31101  unopf1o  31200  adj2  31218  adjvalval  31221  adjlnop  31370  leopmul2i  31419  cvntr  31576  mdsymlem5  31691  sumdmdii  31699  supxrnemnf  32012  odutos  32169  tlt2  32170  tosglblem  32175  archiabl  32375  evls1fpws  32677  unitdivcld  32912  bnj605  33949  bnj607  33958  fisshasheq  34135  swrdrevpfx  34138  cusgredgex  34143  acycgr1v  34171  gcd32  34750  cgrrflx  34990  cgrcom  34993  cgrcomr  35000  btwntriv1  35019  cgr3com  35056  colineartriv2  35071  segleantisym  35118  seglelin  35119  btwnoutside  35128  clsint2  35262  dissneqlem  36269  ftc1anclem5  36613  heibor1  36726  rngoidl  36940  ispridlc  36986  opltcon3b  38122  cmtcomlemN  38166  cmtcomN  38167  cmt3N  38169  cmtbr3N  38172  cvrval2  38192  cvrnbtwn4  38197  leatb  38210  atlrelat1  38239  hlatlej2  38294  hlateq  38318  hlrelat5N  38320  snatpsubN  38669  pmap11  38681  paddcom  38732  sspadd2  38735  paddss12  38738  cdleme51finvN  39475  cdleme51finvtrN  39477  cdlemeiota  39504  cdlemg2jlemOLDN  39512  cdlemg2klem  39514  cdlemg4b1  39528  cdlemg4b2  39529  trljco2  39660  tgrpabl  39670  tendoplcom  39701  cdleml6  39900  erngdvlem3-rN  39917  dia11N  39967  dib11N  40079  dih11  40184  uzindd  40890  lcmineqlem1  40942  nerabdioph  41595  monotoddzzfi  41729  fzneg  41769  jm2.19lem2  41777  ismnushort  43108  nzss  43124  sineq0ALT  43746  opprrng  46722  lincvalsng  47145  reccot  47851