Theorem 3com23 1132

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3coml  1133  3anidm13  1428  eqreu  3670  f1ofveu  7350  curry2f  8047  dfsmo2  8277  nneob  8582  nadd32  8623  f1oeng  8907  domnsymfi  9124  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  php3  9133  fodomfir  9228  suppr  9375  infdif  10121  axdclem2  10433  gchen1  10539  grumap  10722  grudomon  10731  mul32  11303  add32  11356  subsub23  11389  subadd23  11396  addsub12  11397  subsub  11415  subsub3  11417  sub32  11419  suble  11619  lesub  11620  ltsub23  11621  ltsub13  11622  ltleadd  11624  div32  11820  div13  11821  div12  11822  divdiv32  11854  cju  12146  infssuzle  12872  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  fzen  13486  modcyc  13856  expgt0  14048  expge0  14051  expge1  14052  2cshwcom  14769  shftval2  15028  abs3dif  15285  divalgb  16364  submrc  17585  mrieqv2d  17596  pltnlt  18295  pltn2lp  18296  tosso  18374  latnle  18430  latabs1  18432  lubel  18471  ipopos  18493  grpinvcnv  18973  mulgaddcom  19065  mulgneg2  19075  oppgmnd  19320  oddvdsnn0  19510  oddvds  19513  odmulg  19522  odcl2  19531  lsmcomx  19822  srgcom4  20186  srgrmhm  20194  ringcom  20252  mulgass2  20281  opprrng  20316  irredrmul  20398  irredlmul  20399  isdrngrd  20738  isdrngrdOLD  20740  islmodd  20856  lmodcom  20898  rmodislmod  20920  zntoslem  21531  ipcl  21608  evls1fpws  22355  maducoevalmin1  22635  rintopn  22892  opnnei  23103  restin  23149  cnpnei  23247  cnprest  23272  ordthaus  23367  kgen2ss  23538  hausflim  23964  fclsfnflim  24010  cnpfcf  24024  opnsubg  24091  cuspcvg  24283  psmetsym  24293  xmetsym  24330  ngpdsr  24588  ngpds2r  24590  ngpds3r  24592  clmmulg  25086  cphipval2  25226  iscau2  25262  dgr1term  26243  cxpeq0  26660  cxpge0  26665  relogbzcl  26756  negsunif  28065  oldfib  28387  grpoidinvlem2  30594  grpoinvdiv  30626  nvpncan  30743  nvabs  30761  ipval2lem2  30793  dipcj  30803  diporthcom  30805  dipdi  30932  dipassr  30935  dipsubdi  30938  hlipcj  31000  hvadd32  31123  hvsub32  31134  his5  31175  hoadd32  31872  hosubsub  31906  unopf1o  32005  adj2  32023  adjvalval  32026  adjlnop  32175  leopmul2i  32224  cvntr  32381  mdsymlem5  32496  sumdmdii  32504  supxrnemnf  32860  odutos  33047  tlt2  33048  tosglblem  33053  archiabl  33279  unitdivcld  34085  bnj605  35089  bnj607  35098  rankfilimb  35283  r1filim  35285  fisshasheq  35343  swrdrevpfx  35345  cusgredgex  35350  acycgr1v  35377  gcd32  35977  cgrrflx  36215  cgrcom  36218  cgrcomr  36225  btwntriv1  36244  cgr3com  36281  colineartriv2  36296  segleantisym  36343  seglelin  36344  btwnoutside  36353  clsint2  36557  dissneqlem  37702  ftc1anclem5  38064  heibor1  38177  rngoidl  38391  ispridlc  38437  opltcon3b  39696  cmtcomlemN  39740  cmtcomN  39741  cmt3N  39743  cmtbr3N  39746  cvrval2  39766  cvrnbtwn4  39771  leatb  39784  atlrelat1  39813  hlatlej2  39868  hlateq  39891  hlrelat5N  39893  snatpsubN  40242  pmap11  40254  paddcom  40305  sspadd2  40308  paddss12  40311  cdleme51finvN  41048  cdleme51finvtrN  41050  cdlemeiota  41077  cdlemg2jlemOLDN  41085  cdlemg2klem  41087  cdlemg4b1  41101  cdlemg4b2  41102  trljco2  41233  tgrpabl  41243  tendoplcom  41274  cdleml6  41473  erngdvlem3-rN  41490  dia11N  41540  dib11N  41652  dih11  41757  uzindd  42463  lcmineqlem1  42514  nerabdioph  43254  monotoddzzfi  43387  fzneg  43427  jm2.19lem2  43435  ismnushort  44745  nzss  44761  sineq0ALT  45380  lincvalsng  48907  reccot  50248