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  3687  f1ofveu  7352  curry2f  8050  dfsmo2  8279  nneob  8584  nadd32  8625  f1oeng  8907  domnsymfi  9124  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  php3  9133  fodomfir  9228  suppr  9375  infdif  10118  axdclem2  10430  gchen1  10536  grumap  10719  grudomon  10728  mul32  11299  add32  11352  subsub23  11385  subadd23  11392  addsub12  11393  subsub  11411  subsub3  11413  sub32  11415  suble  11615  lesub  11616  ltsub23  11617  ltsub13  11618  ltleadd  11620  div32  11816  div13  11817  div12  11818  divdiv32  11849  cju  12141  infssuzle  12844  ioo0  13286  ico0  13307  ioc0  13308  icc0  13309  fzen  13457  modcyc  13826  expgt0  14018  expge0  14021  expge1  14022  2cshwcom  14739  shftval2  14998  abs3dif  15255  divalgb  16331  submrc  17551  mrieqv2d  17562  pltnlt  18261  pltn2lp  18262  tosso  18340  latnle  18396  latabs1  18398  lubel  18437  ipopos  18459  grpinvcnv  18936  mulgaddcom  19028  mulgneg2  19038  oppgmnd  19283  oddvdsnn0  19473  oddvds  19476  odmulg  19485  odcl2  19494  lsmcomx  19785  srgcom4  20149  srgrmhm  20157  ringcom  20215  mulgass2  20244  opprrng  20281  irredrmul  20363  irredlmul  20364  isdrngrd  20699  isdrngrdOLD  20701  islmodd  20817  lmodcom  20859  rmodislmod  20881  zntoslem  21511  ipcl  21588  evls1fpws  22313  maducoevalmin1  22596  rintopn  22853  opnnei  23064  restin  23110  cnpnei  23208  cnprest  23233  ordthaus  23328  kgen2ss  23499  hausflim  23925  fclsfnflim  23971  cnpfcf  23985  opnsubg  24052  cuspcvg  24244  psmetsym  24254  xmetsym  24291  ngpdsr  24549  ngpds2r  24551  ngpds3r  24553  clmmulg  25057  cphipval2  25197  iscau2  25233  dgr1term  26221  cxpeq0  26643  cxpge0  26648  relogbzcl  26740  negsunif  28051  oldfib  28373  grpoidinvlem2  30580  grpoinvdiv  30612  nvpncan  30729  nvabs  30747  ipval2lem2  30779  dipcj  30789  diporthcom  30791  dipdi  30918  dipassr  30921  dipsubdi  30924  hlipcj  30986  hvadd32  31109  hvsub32  31120  his5  31161  hoadd32  31858  hosubsub  31892  unopf1o  31991  adj2  32009  adjvalval  32012  adjlnop  32161  leopmul2i  32210  cvntr  32367  mdsymlem5  32482  sumdmdii  32490  supxrnemnf  32848  odutos  33050  tlt2  33051  tosglblem  33056  archiabl  33280  unitdivcld  34058  bnj605  35063  bnj607  35072  rankfilimb  35258  r1filim  35260  fisshasheq  35309  swrdrevpfx  35311  cusgredgex  35316  acycgr1v  35343  gcd32  35943  cgrrflx  36181  cgrcom  36184  cgrcomr  36191  btwntriv1  36210  cgr3com  36247  colineartriv2  36262  segleantisym  36309  seglelin  36310  btwnoutside  36319  clsint2  36523  dissneqlem  37545  ftc1anclem5  37898  heibor1  38011  rngoidl  38225  ispridlc  38271  opltcon3b  39464  cmtcomlemN  39508  cmtcomN  39509  cmt3N  39511  cmtbr3N  39514  cvrval2  39534  cvrnbtwn4  39539  leatb  39552  atlrelat1  39581  hlatlej2  39636  hlateq  39659  hlrelat5N  39661  snatpsubN  40010  pmap11  40022  paddcom  40073  sspadd2  40076  paddss12  40079  cdleme51finvN  40816  cdleme51finvtrN  40818  cdlemeiota  40845  cdlemg2jlemOLDN  40853  cdlemg2klem  40855  cdlemg4b1  40869  cdlemg4b2  40870  trljco2  41001  tgrpabl  41011  tendoplcom  41042  cdleml6  41241  erngdvlem3-rN  41258  dia11N  41308  dib11N  41420  dih11  41525  uzindd  42231  lcmineqlem1  42283  nerabdioph  43051  monotoddzzfi  43184  fzneg  43224  jm2.19lem2  43232  ismnushort  44542  nzss  44558  sineq0ALT  45177  lincvalsng  48662  reccot  50003