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  3683  f1ofveu  7340  curry2f  8038  dfsmo2  8267  nneob  8571  nadd32  8612  f1oeng  8893  domnsymfi  9109  sdomdomtrfi  9110  domsdomtrfi  9111  php  9116  php3  9118  fodomfir  9212  suppr  9356  infdif  10099  axdclem2  10411  gchen1  10516  grumap  10699  grudomon  10708  mul32  11279  add32  11332  subsub23  11365  subadd23  11372  addsub12  11373  subsub  11391  subsub3  11393  sub32  11395  suble  11595  lesub  11596  ltsub23  11597  ltsub13  11598  ltleadd  11600  div32  11796  div13  11797  div12  11798  divdiv32  11829  cju  12121  infssuzle  12829  ioo0  13270  ico0  13291  ioc0  13292  icc0  13293  fzen  13441  modcyc  13810  expgt0  14002  expge0  14005  expge1  14006  2cshwcom  14723  shftval2  14982  abs3dif  15239  divalgb  16315  submrc  17534  mrieqv2d  17545  pltnlt  18244  pltn2lp  18245  tosso  18323  latnle  18379  latabs1  18381  lubel  18420  ipopos  18442  grpinvcnv  18919  mulgaddcom  19011  mulgneg2  19021  oppgmnd  19266  oddvdsnn0  19456  oddvds  19459  odmulg  19468  odcl2  19477  lsmcomx  19768  srgcom4  20132  srgrmhm  20140  ringcom  20198  mulgass2  20227  opprrng  20263  irredrmul  20345  irredlmul  20346  isdrngrd  20681  isdrngrdOLD  20683  islmodd  20799  lmodcom  20841  rmodislmod  20863  zntoslem  21493  ipcl  21570  evls1fpws  22284  maducoevalmin1  22567  rintopn  22824  opnnei  23035  restin  23081  cnpnei  23179  cnprest  23204  ordthaus  23299  kgen2ss  23470  hausflim  23896  fclsfnflim  23942  cnpfcf  23956  opnsubg  24023  cuspcvg  24215  psmetsym  24225  xmetsym  24262  ngpdsr  24520  ngpds2r  24522  ngpds3r  24524  clmmulg  25028  cphipval2  25168  iscau2  25204  dgr1term  26192  cxpeq0  26614  cxpge0  26619  relogbzcl  26711  negsunif  27997  grpoidinvlem2  30485  grpoinvdiv  30517  nvpncan  30634  nvabs  30652  ipval2lem2  30684  dipcj  30694  diporthcom  30696  dipdi  30823  dipassr  30826  dipsubdi  30829  hlipcj  30891  hvadd32  31014  hvsub32  31025  his5  31066  hoadd32  31763  hosubsub  31797  unopf1o  31896  adj2  31914  adjvalval  31917  adjlnop  32066  leopmul2i  32115  cvntr  32272  mdsymlem5  32387  sumdmdii  32395  supxrnemnf  32751  odutos  32949  tlt2  32950  tosglblem  32955  archiabl  33167  unitdivcld  33914  bnj605  34919  bnj607  34928  rankfilimb  35113  r1filim  35115  fisshasheq  35159  swrdrevpfx  35161  cusgredgex  35166  acycgr1v  35193  gcd32  35793  cgrrflx  36029  cgrcom  36032  cgrcomr  36039  btwntriv1  36058  cgr3com  36095  colineartriv2  36110  segleantisym  36157  seglelin  36158  btwnoutside  36167  clsint2  36371  dissneqlem  37382  ftc1anclem5  37745  heibor1  37858  rngoidl  38072  ispridlc  38118  opltcon3b  39251  cmtcomlemN  39295  cmtcomN  39296  cmt3N  39298  cmtbr3N  39301  cvrval2  39321  cvrnbtwn4  39326  leatb  39339  atlrelat1  39368  hlatlej2  39423  hlateq  39446  hlrelat5N  39448  snatpsubN  39797  pmap11  39809  paddcom  39860  sspadd2  39863  paddss12  39866  cdleme51finvN  40603  cdleme51finvtrN  40605  cdlemeiota  40632  cdlemg2jlemOLDN  40640  cdlemg2klem  40642  cdlemg4b1  40656  cdlemg4b2  40657  trljco2  40788  tgrpabl  40798  tendoplcom  40829  cdleml6  41028  erngdvlem3-rN  41045  dia11N  41095  dib11N  41207  dih11  41312  uzindd  42018  lcmineqlem1  42070  nerabdioph  42850  monotoddzzfi  42983  fzneg  43023  jm2.19lem2  43031  ismnushort  44342  nzss  44358  sineq0ALT  44977  lincvalsng  48456  reccot  49798