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 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3coml  1127  3anidm13  1420  eqreu  3690  f1ofveu  7356  curry2f  8045  dfsmo2  8298  nneob  8607  nadd32  8648  f1oeng  8918  domnsymfi  9154  sdomdomtrfi  9155  domsdomtrfi  9156  php  9161  php3  9163  suppr  9416  infdif  10154  axdclem2  10465  gchen1  10570  grumap  10753  grudomon  10762  mul32  11330  add32  11382  subsub23  11415  subadd23  11422  addsub12  11423  subsub  11440  subsub3  11442  sub32  11444  suble  11642  lesub  11643  ltsub23  11644  ltsub13  11645  ltleadd  11647  div32  11842  div13  11843  div12  11844  divdiv32  11872  cju  12158  infssuzle  12865  ioo0  13299  ico0  13320  ioc0  13321  icc0  13322  fzen  13468  modcyc  13821  expgt0  14011  expge0  14014  expge1  14015  2cshwcom  14716  shftval2  14972  abs3dif  15228  divalgb  16297  submrc  17522  mrieqv2d  17533  pltnlt  18243  pltn2lp  18244  tosso  18322  latnle  18376  latabs1  18378  lubel  18417  ipopos  18439  grpinvcnv  18829  mulgaddcom  18914  mulgneg2  18924  oppgmnd  19149  oddvdsnn0  19340  oddvds  19343  odmulg  19352  odcl2  19361  lsmcomx  19648  srgcom4  19959  srgrmhm  19967  ringcom  20015  mulgass2  20039  opprring  20074  irredrmul  20152  irredlmul  20153  isdrngrd  20256  isdrngrdOLD  20258  islmodd  20384  lmodcom  20425  rmodislmod  20447  rmodislmodOLD  20448  opprdomn  20808  zntoslem  21000  ipcl  21074  maducoevalmin1  22038  rintopn  22295  opnnei  22508  restin  22554  cnpnei  22652  cnprest  22677  ordthaus  22772  kgen2ss  22943  hausflim  23369  fclsfnflim  23415  cnpfcf  23429  opnsubg  23496  cuspcvg  23690  psmetsym  23700  xmetsym  23737  ngpdsr  23998  ngpds2r  24000  ngpds3r  24002  clmmulg  24501  cphipval2  24642  iscau2  24678  dgr1term  25658  cxpeq0  26070  cxpge0  26075  relogbzcl  26161  negsunif  27393  grpoidinvlem2  29510  grpoinvdiv  29542  nvpncan  29659  nvabs  29677  ipval2lem2  29709  dipcj  29719  diporthcom  29721  dipdi  29848  dipassr  29851  dipsubdi  29854  hlipcj  29916  hvadd32  30039  hvsub32  30050  his5  30091  hoadd32  30788  hosubsub  30822  unopf1o  30921  adj2  30939  adjvalval  30942  adjlnop  31091  leopmul2i  31140  cvntr  31297  mdsymlem5  31412  sumdmdii  31420  supxrnemnf  31741  odutos  31898  tlt2  31899  tosglblem  31904  archiabl  32104  evls1fpws  32348  unitdivcld  32571  bnj605  33608  bnj607  33617  fisshasheq  33794  swrdrevpfx  33797  cusgredgex  33802  acycgr1v  33830  gcd32  34408  cgrrflx  34648  cgrcom  34651  cgrcomr  34658  btwntriv1  34677  cgr3com  34714  colineartriv2  34729  segleantisym  34776  seglelin  34777  btwnoutside  34786  clsint2  34877  dissneqlem  35884  ftc1anclem5  36228  heibor1  36342  rngoidl  36556  ispridlc  36602  opltcon3b  37739  cmtcomlemN  37783  cmtcomN  37784  cmt3N  37786  cmtbr3N  37789  cvrval2  37809  cvrnbtwn4  37814  leatb  37827  atlrelat1  37856  hlatlej2  37911  hlateq  37935  hlrelat5N  37937  snatpsubN  38286  pmap11  38298  paddcom  38349  sspadd2  38352  paddss12  38355  cdleme51finvN  39092  cdleme51finvtrN  39094  cdlemeiota  39121  cdlemg2jlemOLDN  39129  cdlemg2klem  39131  cdlemg4b1  39145  cdlemg4b2  39146  trljco2  39277  tgrpabl  39287  tendoplcom  39318  cdleml6  39517  erngdvlem3-rN  39534  dia11N  39584  dib11N  39696  dih11  39801  uzindd  40507  lcmineqlem1  40559  nerabdioph  41190  monotoddzzfi  41324  fzneg  41364  jm2.19lem2  41372  ismnushort  42703  nzss  42719  sineq0ALT  43341  lincvalsng  46617  reccot  47323