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  3689  f1ofveu  7343  curry2f  8041  dfsmo2  8270  nneob  8574  nadd32  8615  f1oeng  8896  domnsymfi  9114  sdomdomtrfi  9115  domsdomtrfi  9116  php  9121  php3  9123  fodomfir  9218  suppr  9362  infdif  10102  axdclem2  10414  gchen1  10519  grumap  10702  grudomon  10711  mul32  11282  add32  11335  subsub23  11368  subadd23  11375  addsub12  11376  subsub  11394  subsub3  11396  sub32  11398  suble  11598  lesub  11599  ltsub23  11600  ltsub13  11601  ltleadd  11603  div32  11799  div13  11800  div12  11801  divdiv32  11832  cju  12124  infssuzle  12832  ioo0  13273  ico0  13294  ioc0  13295  icc0  13296  fzen  13444  modcyc  13810  expgt0  14002  expge0  14005  expge1  14006  2cshwcom  14722  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  18885  mulgaddcom  18977  mulgneg2  18987  oppgmnd  19233  oddvdsnn0  19423  oddvds  19426  odmulg  19435  odcl2  19444  lsmcomx  19735  srgcom4  20099  srgrmhm  20107  ringcom  20165  mulgass2  20194  opprrng  20230  irredrmul  20312  irredlmul  20313  isdrngrd  20651  isdrngrdOLD  20653  islmodd  20769  lmodcom  20811  rmodislmod  20833  zntoslem  21463  ipcl  21540  evls1fpws  22254  maducoevalmin1  22537  rintopn  22794  opnnei  23005  restin  23051  cnpnei  23149  cnprest  23174  ordthaus  23269  kgen2ss  23440  hausflim  23866  fclsfnflim  23912  cnpfcf  23926  opnsubg  23993  cuspcvg  24186  psmetsym  24196  xmetsym  24233  ngpdsr  24491  ngpds2r  24493  ngpds3r  24495  clmmulg  24999  cphipval2  25139  iscau2  25175  dgr1term  26163  cxpeq0  26585  cxpge0  26590  relogbzcl  26682  negsunif  27966  grpoidinvlem2  30449  grpoinvdiv  30481  nvpncan  30598  nvabs  30616  ipval2lem2  30648  dipcj  30658  diporthcom  30660  dipdi  30787  dipassr  30790  dipsubdi  30793  hlipcj  30855  hvadd32  30978  hvsub32  30989  his5  31030  hoadd32  31727  hosubsub  31761  unopf1o  31860  adj2  31878  adjvalval  31881  adjlnop  32030  leopmul2i  32079  cvntr  32236  mdsymlem5  32351  sumdmdii  32359  supxrnemnf  32711  odutos  32910  tlt2  32911  tosglblem  32916  archiabl  33140  unitdivcld  33868  bnj605  34874  bnj607  34883  fisshasheq  35088  swrdrevpfx  35090  cusgredgex  35095  acycgr1v  35122  gcd32  35722  cgrrflx  35961  cgrcom  35964  cgrcomr  35971  btwntriv1  35990  cgr3com  36027  colineartriv2  36042  segleantisym  36089  seglelin  36090  btwnoutside  36099  clsint2  36303  dissneqlem  37314  ftc1anclem5  37677  heibor1  37790  rngoidl  38004  ispridlc  38050  opltcon3b  39183  cmtcomlemN  39227  cmtcomN  39228  cmt3N  39230  cmtbr3N  39233  cvrval2  39253  cvrnbtwn4  39258  leatb  39271  atlrelat1  39300  hlatlej2  39355  hlateq  39378  hlrelat5N  39380  snatpsubN  39729  pmap11  39741  paddcom  39792  sspadd2  39795  paddss12  39798  cdleme51finvN  40535  cdleme51finvtrN  40537  cdlemeiota  40564  cdlemg2jlemOLDN  40572  cdlemg2klem  40574  cdlemg4b1  40588  cdlemg4b2  40589  trljco2  40720  tgrpabl  40730  tendoplcom  40761  cdleml6  40960  erngdvlem3-rN  40977  dia11N  41027  dib11N  41139  dih11  41244  uzindd  41950  lcmineqlem1  42002  nerabdioph  42782  monotoddzzfi  42915  fzneg  42955  jm2.19lem2  42963  ismnushort  44274  nzss  44290  sineq0ALT  44910  lincvalsng  48401  reccot  49743