Theorem 3com23 1126

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3coml  1127  3anidm13  1422  eqreu  3700  f1ofveu  7381  curry2f  8087  dfsmo2  8316  nneob  8620  nadd32  8661  f1oeng  8942  domnsymfi  9164  sdomdomtrfi  9165  domsdomtrfi  9166  php  9171  php3  9173  fodomfir  9279  suppr  9423  infdif  10161  axdclem2  10473  gchen1  10578  grumap  10761  grudomon  10770  mul32  11340  add32  11393  subsub23  11426  subadd23  11433  addsub12  11434  subsub  11452  subsub3  11454  sub32  11456  suble  11656  lesub  11657  ltsub23  11658  ltsub13  11659  ltleadd  11661  div32  11857  div13  11858  div12  11859  divdiv32  11890  cju  12182  infssuzle  12890  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  fzen  13502  modcyc  13868  expgt0  14060  expge0  14063  expge1  14064  2cshwcom  14781  shftval2  15041  abs3dif  15298  divalgb  16374  submrc  17589  mrieqv2d  17600  pltnlt  18299  pltn2lp  18300  tosso  18378  latnle  18432  latabs1  18434  lubel  18473  ipopos  18495  grpinvcnv  18938  mulgaddcom  19030  mulgneg2  19040  oppgmnd  19286  oddvdsnn0  19474  oddvds  19477  odmulg  19486  odcl2  19495  lsmcomx  19786  srgcom4  20123  srgrmhm  20131  ringcom  20189  mulgass2  20218  opprrng  20254  irredrmul  20336  irredlmul  20337  isdrngrd  20675  isdrngrdOLD  20677  islmodd  20772  lmodcom  20814  rmodislmod  20836  zntoslem  21466  ipcl  21542  evls1fpws  22256  maducoevalmin1  22539  rintopn  22796  opnnei  23007  restin  23053  cnpnei  23151  cnprest  23176  ordthaus  23271  kgen2ss  23442  hausflim  23868  fclsfnflim  23914  cnpfcf  23928  opnsubg  23995  cuspcvg  24188  psmetsym  24198  xmetsym  24235  ngpdsr  24493  ngpds2r  24495  ngpds3r  24497  clmmulg  25001  cphipval2  25141  iscau2  25177  dgr1term  26165  cxpeq0  26587  cxpge0  26592  relogbzcl  26684  negsunif  27961  grpoidinvlem2  30434  grpoinvdiv  30466  nvpncan  30583  nvabs  30601  ipval2lem2  30633  dipcj  30643  diporthcom  30645  dipdi  30772  dipassr  30775  dipsubdi  30778  hlipcj  30840  hvadd32  30963  hvsub32  30974  his5  31015  hoadd32  31712  hosubsub  31746  unopf1o  31845  adj2  31863  adjvalval  31866  adjlnop  32015  leopmul2i  32064  cvntr  32221  mdsymlem5  32336  sumdmdii  32344  supxrnemnf  32691  odutos  32894  tlt2  32895  tosglblem  32900  archiabl  33152  unitdivcld  33891  bnj605  34897  bnj607  34906  fisshasheq  35102  swrdrevpfx  35104  cusgredgex  35109  acycgr1v  35136  gcd32  35736  cgrrflx  35975  cgrcom  35978  cgrcomr  35985  btwntriv1  36004  cgr3com  36041  colineartriv2  36056  segleantisym  36103  seglelin  36104  btwnoutside  36113  clsint2  36317  dissneqlem  37328  ftc1anclem5  37691  heibor1  37804  rngoidl  38018  ispridlc  38064  opltcon3b  39197  cmtcomlemN  39241  cmtcomN  39242  cmt3N  39244  cmtbr3N  39247  cvrval2  39267  cvrnbtwn4  39272  leatb  39285  atlrelat1  39314  hlatlej2  39369  hlateq  39393  hlrelat5N  39395  snatpsubN  39744  pmap11  39756  paddcom  39807  sspadd2  39810  paddss12  39813  cdleme51finvN  40550  cdleme51finvtrN  40552  cdlemeiota  40579  cdlemg2jlemOLDN  40587  cdlemg2klem  40589  cdlemg4b1  40603  cdlemg4b2  40604  trljco2  40735  tgrpabl  40745  tendoplcom  40776  cdleml6  40975  erngdvlem3-rN  40992  dia11N  41042  dib11N  41154  dih11  41259  uzindd  41965  lcmineqlem1  42017  nerabdioph  42797  monotoddzzfi  42931  fzneg  42971  jm2.19lem2  42979  ismnushort  44290  nzss  44306  sineq0ALT  44926  lincvalsng  48405  reccot  49747