Theorem 3com23 1142

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3coml  1143  3anidm13  1445  eqreu  3701  f1ofveu  7405  curry2f  8102  dfsmo2  8333  nneob  8641  nadd32  8683  f1oeng  8966  domnsymfi  9183  sdomdomtrfi  9184  domsdomtrfi  9185  php  9190  php3  9192  fodomfir  9286  suppr  9431  infdif  10190  axdclem2  10503  gchen1  10609  grumap  10792  grudomon  10801  mul32  11375  add32  11428  subsub23  11461  subadd23  11468  addsub12  11469  subsub  11487  subsub3  11489  sub32  11491  suble  11691  lesub  11692  ltsub23  11693  ltsub13  11694  ltleadd  11696  div32  11891  div13  11892  div12  11893  divdiv32  11922  cju  12213  infssuzle  12954  ioo0  13396  ico0  13417  ioc0  13418  icc0  13419  fzen  13568  modcyc  13938  expgt0  14130  expge0  14133  expge1  14134  2cshwcom  14852  shftval2  15111  abs3dif  15382  divalgb  16461  submrc  17683  mrieqv2d  17694  pltnlt  18393  pltn2lp  18394  tosso  18472  latnle  18528  latabs1  18530  lubel  18569  ipopos  18591  grpinvcnv  19072  mulgaddcom  19163  mulgneg2  19173  oppgmnd  19423  oddvdsnn0  19613  oddvds  19616  odmulg  19625  odcl2  19634  lsmcomx  19925  srgcom4  20295  srgrmhm  20303  ringcom  20362  mulgass2  20391  opprrng  20426  irredrmul  20508  irredlmul  20509  isdrngrd  20847  isdrngrdOLD  20849  islmodd  20964  lmodcom  21006  rmodislmod  21028  zntoslem  21674  ipcl  21751  evls1fpws  22497  maducoevalmin1  22777  rintopn  23034  opnnei  23245  restin  23291  cnpnei  23389  cnprest  23414  ordthaus  23509  kgen2ss  23680  hausflim  24106  fclsfnflim  24152  cnpfcf  24166  opnsubg  24233  cuspcvg  24425  psmetsym  24435  xmetsym  24472  ngpdsr  24730  ngpds2r  24732  ngpds3r  24734  clmmulg  25228  cphipval2  25368  iscau2  25404  dgr1term  26385  cxpeq0  26808  cxpge0  26813  relogbzcl  26904  negsunif  28213  oldfib  28535  grpoidinvlem2  30797  grpoinvdiv  30829  nvpncan  30946  nvabs  30964  ipval2lem2  30996  dipcj  31006  diporthcom  31008  dipdi  31135  dipassr  31138  dipsubdi  31141  hlipcj  31203  hvadd32  31326  hvsub32  31337  his5  31378  hoadd32  32075  hosubsub  32109  unopf1o  32208  adj2  32226  adjvalval  32229  adjlnop  32378  leopmul2i  32427  cvntr  32584  mdsymlem5  32699  sumdmdii  32707  supxrnemnf  33053  odutos  33228  tlt2  33229  tosglblem  33234  archiabl  33458  unitdivcld  34235  bnj605  35239  bnj607  35248  rankfilimb  35437  r1filim  35439  fisshasheq  35504  swrdrevpfx  35506  cusgredgex  35512  acycgr1v  35539  gcd32  36139  cgrrflx  36377  cgrcom  36380  cgrcomr  36387  btwntriv1  36406  cgr3com  36443  colineartriv2  36458  segleantisym  36505  seglelin  36506  btwnoutside  36515  clsint2  36728  dissneqlem  37873  ftc1anclem5  38235  heibor1  38348  rngoidl  38562  ispridlc  38608  opltcon3b  39867  cmtcomlemN  39911  cmtcomN  39912  cmt3N  39914  cmtbr3N  39917  cvrval2  39937  cvrnbtwn4  39942  leatb  39955  atlrelat1  39984  hlatlej2  40039  hlateq  40062  hlrelat5N  40064  snatpsubN  40413  pmap11  40425  paddcom  40476  sspadd2  40479  paddss12  40482  cdleme51finvN  41219  cdleme51finvtrN  41221  cdlemeiota  41248  cdlemg2jlemOLDN  41256  cdlemg2klem  41258  cdlemg4b1  41272  cdlemg4b2  41273  trljco2  41404  tgrpabl  41414  tendoplcom  41445  cdleml6  41644  erngdvlem3-rN  41661  dia11N  41711  dib11N  41823  dih11  41928  uzindd  42634  lcmineqlem1  42685  nerabdioph  43427  monotoddzzfi  43560  fzneg  43600  jm2.19lem2  43608  ismnushort  44902  nzss  44918  sineq0ALT  45536  lincvalsng  49080  reccot  50420