Theorem 3com23 1127

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3coml  1128  3anidm13  1423  eqreu  3689  f1ofveu  7364  curry2f  8062  dfsmo2  8291  nneob  8596  nadd32  8637  f1oeng  8921  domnsymfi  9138  sdomdomtrfi  9139  domsdomtrfi  9140  php  9145  php3  9147  fodomfir  9242  suppr  9389  infdif  10132  axdclem2  10444  gchen1  10550  grumap  10733  grudomon  10742  mul32  11313  add32  11366  subsub23  11399  subadd23  11406  addsub12  11407  subsub  11425  subsub3  11427  sub32  11429  suble  11629  lesub  11630  ltsub23  11631  ltsub13  11632  ltleadd  11634  div32  11830  div13  11831  div12  11832  divdiv32  11863  cju  12155  infssuzle  12858  ioo0  13300  ico0  13321  ioc0  13322  icc0  13323  fzen  13471  modcyc  13840  expgt0  14032  expge0  14035  expge1  14036  2cshwcom  14753  shftval2  15012  abs3dif  15269  divalgb  16345  submrc  17565  mrieqv2d  17576  pltnlt  18275  pltn2lp  18276  tosso  18354  latnle  18410  latabs1  18412  lubel  18451  ipopos  18473  grpinvcnv  18953  mulgaddcom  19045  mulgneg2  19055  oppgmnd  19300  oddvdsnn0  19490  oddvds  19493  odmulg  19502  odcl2  19511  lsmcomx  19802  srgcom4  20166  srgrmhm  20174  ringcom  20232  mulgass2  20261  opprrng  20298  irredrmul  20380  irredlmul  20381  isdrngrd  20716  isdrngrdOLD  20718  islmodd  20834  lmodcom  20876  rmodislmod  20898  zntoslem  21528  ipcl  21605  evls1fpws  22330  maducoevalmin1  22613  rintopn  22870  opnnei  23081  restin  23127  cnpnei  23225  cnprest  23250  ordthaus  23345  kgen2ss  23516  hausflim  23942  fclsfnflim  23988  cnpfcf  24002  opnsubg  24069  cuspcvg  24261  psmetsym  24271  xmetsym  24308  ngpdsr  24566  ngpds2r  24568  ngpds3r  24570  clmmulg  25074  cphipval2  25214  iscau2  25250  dgr1term  26238  cxpeq0  26660  cxpge0  26665  relogbzcl  26757  negsunif  28068  oldfib  28390  grpoidinvlem2  30599  grpoinvdiv  30631  nvpncan  30748  nvabs  30766  ipval2lem2  30798  dipcj  30808  diporthcom  30810  dipdi  30937  dipassr  30940  dipsubdi  30943  hlipcj  31005  hvadd32  31128  hvsub32  31139  his5  31180  hoadd32  31877  hosubsub  31911  unopf1o  32010  adj2  32028  adjvalval  32031  adjlnop  32180  leopmul2i  32229  cvntr  32386  mdsymlem5  32501  sumdmdii  32509  supxrnemnf  32865  odutos  33067  tlt2  33068  tosglblem  33073  archiabl  33298  unitdivcld  34085  bnj605  35089  bnj607  35098  rankfilimb  35285  r1filim  35287  fisshasheq  35337  swrdrevpfx  35339  cusgredgex  35344  acycgr1v  35371  gcd32  35971  cgrrflx  36209  cgrcom  36212  cgrcomr  36219  btwntriv1  36238  cgr3com  36275  colineartriv2  36290  segleantisym  36337  seglelin  36338  btwnoutside  36347  clsint2  36551  dissneqlem  37622  ftc1anclem5  37977  heibor1  38090  rngoidl  38304  ispridlc  38350  opltcon3b  39609  cmtcomlemN  39653  cmtcomN  39654  cmt3N  39656  cmtbr3N  39659  cvrval2  39679  cvrnbtwn4  39684  leatb  39697  atlrelat1  39726  hlatlej2  39781  hlateq  39804  hlrelat5N  39806  snatpsubN  40155  pmap11  40167  paddcom  40218  sspadd2  40221  paddss12  40224  cdleme51finvN  40961  cdleme51finvtrN  40963  cdlemeiota  40990  cdlemg2jlemOLDN  40998  cdlemg2klem  41000  cdlemg4b1  41014  cdlemg4b2  41015  trljco2  41146  tgrpabl  41156  tendoplcom  41187  cdleml6  41386  erngdvlem3-rN  41403  dia11N  41453  dib11N  41565  dih11  41670  uzindd  42376  lcmineqlem1  42428  nerabdioph  43195  monotoddzzfi  43328  fzneg  43368  jm2.19lem2  43376  ismnushort  44686  nzss  44702  sineq0ALT  45321  lincvalsng  48805  reccot  50146