Theorem 3com23 1144

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3coml  1145  3anidm13  1447  eqreu  3687  f1ofveu  7414  curry2f  8119  dfsmo2  8355  nneob  8665  nadd32  8707  f1oeng  8997  domnsymfi  9215  sdomdomtrfi  9216  domsdomtrfi  9217  php  9222  php3  9224  fodomfir  9319  suppr  9464  infdif  10286  axdclem2  10598  gchen1  10710  grumap  10893  grudomon  10902  mul32  11476  add32  11529  subsub23  11562  subadd23  11569  addsub12  11570  subsub  11588  subsub3  11590  sub32  11592  suble  11794  lesub  11795  ltsub23  11796  ltsub13  11797  ltleadd  11799  div32  11994  div13  11995  div12  11996  divdiv32  12025  cju  12316  infssuzle  13058  ioo0  13501  ico0  13522  ioc0  13523  icc0  13524  fzen  13674  modcyc  14046  expgt0  14238  expge0  14241  expge1  14242  swrdrevpfx  14918  2cshwcom  14967  shftval2  15228  abs3dif  15499  divalgb  16574  submrc  17802  mrieqv2d  17813  pltnlt  18512  pltn2lp  18513  tosso  18591  latnle  18647  latabs1  18649  lubel  18688  ipopos  18710  grpinvcnv  19217  mulgaddcom  19308  mulgneg2  19318  oppgmnd  19568  oddvdsnn0  19758  oddvds  19761  odmulg  19770  odcl2  19779  lsmcomx  20070  srgcom4  20440  srgrmhm  20448  ringcom  20509  mulgass2  20540  opprrng  20575  irredrmul  20657  irredlmul  20658  isdrngrd  21023  isdrngrdOLD  21025  islmodd  21141  lmodcom  21183  rmodislmod  21205  zntoslem  21862  ipcl  21939  evls1fpws  22687  maducoevalmin1  22967  rintopn  23227  opnnei  23438  restin  23484  cnpnei  23582  cnprest  23607  ordthaus  23702  kgen2ss  23874  hausflim  24300  fclsfnflim  24346  cnpfcf  24360  opnsubg  24427  cuspcvg  24619  psmetsym  24629  xmetsym  24666  ngpdsr  24924  ngpds2r  24926  ngpds3r  24928  clmmulg  25422  cphipval2  25562  iscau2  25598  dgr1term  26579  cxpeq0  27006  cxpge0  27011  relogbzcl  27102  negsunif  28441  oldfib  28763  grpoidinvlem2  31107  grpoinvdiv  31139  nvpncan  31256  nvabs  31274  ipval2lem2  31306  dipcj  31316  diporthcom  31318  dipdi  31445  dipassr  31448  dipsubdi  31451  hlipcj  31513  hvadd32  31636  hvsub32  31647  his5  31688  hoadd32  32385  hosubsub  32419  unopf1o  32518  adj2  32536  adjvalval  32539  adjlnop  32688  leopmul2i  32737  cvntr  32894  mdsymlem5  33009  sumdmdii  33017  supxrnemnf  33360  odutos  33529  tlt2  33530  tosglblem  33535  archiabl  33759  unitdivcld  34533  bnj605  35537  bnj607  35546  rankfilimb  35728  r1filim  35729  fisshasheq  35903  cusgredgex  35906  acycgr1v  35914  gcd32  36514  cgrrflx  36752  cgrcom  36755  cgrcomr  36762  btwntriv1  36781  cgr3com  36818  colineartriv2  36833  segleantisym  36880  seglelin  36881  btwnoutside  36890  clsint2  37117  dissneqlem  38263  ftc1anclem5  38615  heibor1  38744  rngoidl  38958  ispridlc  39004  opltcon3b  40261  cmtcomlemN  40305  cmtcomN  40306  cmt3N  40308  cmtbr3N  40311  cvrval2  40331  cvrnbtwn4  40336  leatb  40349  atlrelat1  40378  hlatlej2  40433  hlateq  40456  hlrelat5N  40458  snatpsubN  40807  pmap11  40819  paddcom  40870  sspadd2  40873  paddss12  40876  cdleme51finvN  41613  cdleme51finvtrN  41615  cdlemeiota  41642  cdlemg2jlemOLDN  41650  cdlemg2klem  41652  cdlemg4b1  41666  cdlemg4b2  41667  trljco2  41798  tgrpabl  41808  tendoplcom  41839  cdleml6  42038  erngdvlem3-rN  42055  dia11N  42105  dib11N  42217  dih11  42322  uzindd  43028  lcmineqlem1  43079  nerabdioph  43815  monotoddzzfi  43948  fzneg  43988  jm2.19lem2  43996  ismnushort  45284  nzss  45300  sineq0ALT  45918  lincvalsng  49527  reccot  50850