Theorem 3com23 1144

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  3coml  1145  3anidm13  1447  eqreu  3692  f1ofveu  7404  curry2f  8099  dfsmo2  8330  nneob  8638  nadd32  8680  f1oeng  8963  domnsymfi  9180  sdomdomtrfi  9181  domsdomtrfi  9182  php  9187  php3  9189  fodomfir  9283  suppr  9428  infdif  10187  axdclem2  10499  gchen1  10605  grumap  10788  grudomon  10797  mul32  11371  add32  11424  subsub23  11457  subadd23  11464  addsub12  11465  subsub  11483  subsub3  11485  sub32  11487  suble  11687  lesub  11688  ltsub23  11689  ltsub13  11690  ltleadd  11692  div32  11887  div13  11888  div12  11889  divdiv32  11918  cju  12209  infssuzle  12950  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  fzen  13564  modcyc  13935  expgt0  14127  expge0  14130  expge1  14131  2cshwcom  14849  shftval2  15108  abs3dif  15379  divalgb  16457  submrc  17679  mrieqv2d  17690  pltnlt  18389  pltn2lp  18390  tosso  18468  latnle  18524  latabs1  18526  lubel  18565  ipopos  18587  grpinvcnv  19068  mulgaddcom  19159  mulgneg2  19169  oppgmnd  19419  oddvdsnn0  19609  oddvds  19612  odmulg  19621  odcl2  19630  lsmcomx  19921  srgcom4  20291  srgrmhm  20299  ringcom  20359  mulgass2  20388  opprrng  20423  irredrmul  20505  irredlmul  20506  isdrngrd  20869  isdrngrdOLD  20871  islmodd  20987  lmodcom  21029  rmodislmod  21051  zntoslem  21706  ipcl  21783  evls1fpws  22529  maducoevalmin1  22809  rintopn  23066  opnnei  23277  restin  23323  cnpnei  23421  cnprest  23446  ordthaus  23541  kgen2ss  23712  hausflim  24138  fclsfnflim  24184  cnpfcf  24198  opnsubg  24265  cuspcvg  24457  psmetsym  24467  xmetsym  24504  ngpdsr  24762  ngpds2r  24764  ngpds3r  24766  clmmulg  25260  cphipval2  25400  iscau2  25436  dgr1term  26417  cxpeq0  26843  cxpge0  26848  relogbzcl  26939  negsunif  28248  oldfib  28570  grpoidinvlem2  30857  grpoinvdiv  30889  nvpncan  31006  nvabs  31024  ipval2lem2  31056  dipcj  31066  diporthcom  31068  dipdi  31195  dipassr  31198  dipsubdi  31201  hlipcj  31263  hvadd32  31386  hvsub32  31397  his5  31438  hoadd32  32135  hosubsub  32169  unopf1o  32268  adj2  32286  adjvalval  32289  adjlnop  32438  leopmul2i  32487  cvntr  32644  mdsymlem5  32759  sumdmdii  32767  supxrnemnf  33113  odutos  33288  tlt2  33289  tosglblem  33294  archiabl  33518  unitdivcld  34291  bnj605  35295  bnj607  35304  rankfilimb  35496  r1filim  35498  fisshasheq  35606  swrdrevpfx  35608  cusgredgex  35614  acycgr1v  35641  gcd32  36241  cgrrflx  36479  cgrcom  36482  cgrcomr  36489  btwntriv1  36508  cgr3com  36545  colineartriv2  36560  segleantisym  36607  seglelin  36608  btwnoutside  36617  clsint2  36840  dissneqlem  37986  ftc1anclem5  38348  heibor1  38461  rngoidl  38675  ispridlc  38721  opltcon3b  39978  cmtcomlemN  40022  cmtcomN  40023  cmt3N  40025  cmtbr3N  40028  cvrval2  40048  cvrnbtwn4  40053  leatb  40066  atlrelat1  40095  hlatlej2  40150  hlateq  40173  hlrelat5N  40175  snatpsubN  40524  pmap11  40536  paddcom  40587  sspadd2  40590  paddss12  40593  cdleme51finvN  41330  cdleme51finvtrN  41332  cdlemeiota  41359  cdlemg2jlemOLDN  41367  cdlemg2klem  41369  cdlemg4b1  41383  cdlemg4b2  41384  trljco2  41515  tgrpabl  41525  tendoplcom  41556  cdleml6  41755  erngdvlem3-rN  41772  dia11N  41822  dib11N  41934  dih11  42039  uzindd  42745  lcmineqlem1  42796  nerabdioph  43536  monotoddzzfi  43669  fzneg  43709  jm2.19lem2  43717  ismnushort  45011  nzss  45027  sineq0ALT  45645  lincvalsng  49196  reccot  50536