Theorem 3com23 1147

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

Syntax hints:   → wi 4   ∧ w3a 1098

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 198  df-an 384  df-3an 1100

This theorem is referenced by:  3coml  1148  syld3an2OLD  1522  3anidm13  1533  eqreu  3556  f1ofveu  6807  curry2f  7445  dfsmo2  7618  nneob  7907  f1oeng  8149  suppr  8554  infdif  9254  axdclem2  9565  gchen1  9670  grumap  9853  grudomon  9862  mul32  10426  add32  10477  subsub23  10509  subadd23  10516  addsub12  10517  subsub  10534  subsub3  10536  sub32  10538  suble  10729  lesub  10730  ltsub23  10731  ltsub13  10732  ltleadd  10734  div32  10928  div13  10929  div12  10930  divdiv32  10956  cju  11239  infssuzle  11996  ioo0  12424  ico0  12445  ioc0  12446  icc0  12447  fzen  12587  modcyc  12935  expgt0  13122  expge0  13125  expge1  13126  2cshwcom  13793  shftval2  14045  abs3dif  14301  divalgb  15357  submrc  16516  mrieqv2d  16527  pltnlt  17196  pltn2lp  17197  tosso  17264  latnle  17313  latabs1  17315  lubel  17350  ipopos  17388  grpinvcnv  17711  mulgneg2  17803  oppgmnd  18011  oddvdsnn0  18190  oddvds  18193  odmulg  18200  odcl2  18209  lsmcomx  18486  srgrmhm  18764  ringcom  18807  mulgass2  18829  opprring  18859  irredrmul  18935  irredlmul  18936  isdrngrd  19003  islmodd  19099  lmodcom  19139  rmodislmod  19161  opprdomn  19536  zntoslem  20140  ipcl  20215  maducoevalmin1  20697  rintopn  20954  opnnei  21165  restin  21211  cnpnei  21309  cnprest  21334  ordthaus  21429  kgen2ss  21599  hausflim  22025  fclsfnflim  22071  cnpfcf  22085  opnsubg  22151  cuspcvg  22345  psmetsym  22355  xmetsym  22392  ngpdsr  22649  ngpds2r  22651  ngpds3r  22653  clmmulg  23140  cphipval2  23279  iscau2  23314  dgr1term  24257  cxpeq0  24666  cxpge0  24671  relogbzcl  24754  grpoidinvlem2  27716  grpoinvdiv  27748  nvpncan  27866  nvabs  27884  ipval2lem2  27916  dipcj  27926  diporthcom  27928  dipdi  28055  dipassr  28058  dipsubdi  28061  hlipcj  28124  hvadd32  28248  hvsub32  28259  his5  28300  hoadd32  28999  hosubsub  29033  unopf1o  29132  adj2  29150  adjvalval  29153  adjlnop  29302  leopmul2i  29351  cvntr  29508  mdsymlem5  29623  sumdmdii  29631  supxrnemnf  29891  odutos  30020  tlt2  30021  tosglblem  30026  archiabl  30109  unitdivcld  30304  bnj605  31332  bnj607  31341  gcd32  31992  cgrrflx  32448  cgrcom  32451  cgrcomr  32458  btwntriv1  32477  cgr3com  32514  colineartriv2  32529  segleantisym  32576  seglelin  32577  btwnoutside  32586  clsint2  32678  dissneqlem  33541  ftc1anclem5  33838  heibor1  33957  rngoidl  34171  ispridlc  34217  opltcon3b  35028  cmtcomlemN  35072  cmtcomN  35073  cmt3N  35075  cmtbr3N  35078  cvrval2  35098  cvrnbtwn4  35103  leatb  35116  atlrelat1  35145  hlatlej2  35200  hlateq  35223  hlrelat5N  35225  snatpsubN  35574  pmap11  35586  paddcom  35637  sspadd2  35640  paddss12  35643  cdleme51finvN  36381  cdleme51finvtrN  36383  cdlemeiota  36410  cdlemg2jlemOLDN  36418  cdlemg2klem  36420  cdlemg4b1  36434  cdlemg4b2  36435  trljco2  36566  tgrpabl  36576  tendoplcom  36607  cdleml6  36806  erngdvlem3-rN  36823  dia11N  36873  dib11N  36985  dih11  37090  nerabdioph  37914  monotoddzzfi  38048  fzneg  38090  jm2.19lem2  38098  nzss  39056  sineq0ALT  39707  lincvalsng  42757  reccot  43054