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  3697  f1ofveu  7363  curry2f  8064  dfsmo2  8293  nneob  8597  nadd32  8638  f1oeng  8919  domnsymfi  9141  sdomdomtrfi  9142  domsdomtrfi  9143  php  9148  php3  9150  fodomfir  9255  suppr  9399  infdif  10137  axdclem2  10449  gchen1  10554  grumap  10737  grudomon  10746  mul32  11316  add32  11369  subsub23  11402  subadd23  11409  addsub12  11410  subsub  11428  subsub3  11430  sub32  11432  suble  11632  lesub  11633  ltsub23  11634  ltsub13  11635  ltleadd  11637  div32  11833  div13  11834  div12  11835  divdiv32  11866  cju  12158  infssuzle  12866  ioo0  13307  ico0  13328  ioc0  13329  icc0  13330  fzen  13478  modcyc  13844  expgt0  14036  expge0  14039  expge1  14040  2cshwcom  14757  shftval2  15017  abs3dif  15274  divalgb  16350  submrc  17565  mrieqv2d  17576  pltnlt  18275  pltn2lp  18276  tosso  18354  latnle  18408  latabs1  18410  lubel  18449  ipopos  18471  grpinvcnv  18914  mulgaddcom  19006  mulgneg2  19016  oppgmnd  19262  oddvdsnn0  19450  oddvds  19453  odmulg  19462  odcl2  19471  lsmcomx  19762  srgcom4  20099  srgrmhm  20107  ringcom  20165  mulgass2  20194  opprrng  20230  irredrmul  20312  irredlmul  20313  isdrngrd  20651  isdrngrdOLD  20653  islmodd  20748  lmodcom  20790  rmodislmod  20812  zntoslem  21442  ipcl  21518  evls1fpws  22232  maducoevalmin1  22515  rintopn  22772  opnnei  22983  restin  23029  cnpnei  23127  cnprest  23152  ordthaus  23247  kgen2ss  23418  hausflim  23844  fclsfnflim  23890  cnpfcf  23904  opnsubg  23971  cuspcvg  24164  psmetsym  24174  xmetsym  24211  ngpdsr  24469  ngpds2r  24471  ngpds3r  24473  clmmulg  24977  cphipval2  25117  iscau2  25153  dgr1term  26141  cxpeq0  26563  cxpge0  26568  relogbzcl  26660  negsunif  27937  grpoidinvlem2  30407  grpoinvdiv  30439  nvpncan  30556  nvabs  30574  ipval2lem2  30606  dipcj  30616  diporthcom  30618  dipdi  30745  dipassr  30748  dipsubdi  30751  hlipcj  30813  hvadd32  30936  hvsub32  30947  his5  30988  hoadd32  31685  hosubsub  31719  unopf1o  31818  adj2  31836  adjvalval  31839  adjlnop  31988  leopmul2i  32037  cvntr  32194  mdsymlem5  32309  sumdmdii  32317  supxrnemnf  32664  odutos  32867  tlt2  32868  tosglblem  32873  archiabl  33125  unitdivcld  33864  bnj605  34870  bnj607  34879  fisshasheq  35075  swrdrevpfx  35077  cusgredgex  35082  acycgr1v  35109  gcd32  35709  cgrrflx  35948  cgrcom  35951  cgrcomr  35958  btwntriv1  35977  cgr3com  36014  colineartriv2  36029  segleantisym  36076  seglelin  36077  btwnoutside  36086  clsint2  36290  dissneqlem  37301  ftc1anclem5  37664  heibor1  37777  rngoidl  37991  ispridlc  38037  opltcon3b  39170  cmtcomlemN  39214  cmtcomN  39215  cmt3N  39217  cmtbr3N  39220  cvrval2  39240  cvrnbtwn4  39245  leatb  39258  atlrelat1  39287  hlatlej2  39342  hlateq  39366  hlrelat5N  39368  snatpsubN  39717  pmap11  39729  paddcom  39780  sspadd2  39783  paddss12  39786  cdleme51finvN  40523  cdleme51finvtrN  40525  cdlemeiota  40552  cdlemg2jlemOLDN  40560  cdlemg2klem  40562  cdlemg4b1  40576  cdlemg4b2  40577  trljco2  40708  tgrpabl  40718  tendoplcom  40749  cdleml6  40948  erngdvlem3-rN  40965  dia11N  41015  dib11N  41127  dih11  41232  uzindd  41938  lcmineqlem1  41990  nerabdioph  42770  monotoddzzfi  42904  fzneg  42944  jm2.19lem2  42952  ismnushort  44263  nzss  44279  sineq0ALT  44899  lincvalsng  48378  reccot  49720