Theorem 3com23 1123

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3coml  1124  3anidm13  1417  eqreu  3721  f1ofveu  7413  curry2f  8113  dfsmo2  8368  nneob  8677  nadd32  8718  f1oeng  8992  domnsymfi  9228  sdomdomtrfi  9229  domsdomtrfi  9230  php  9235  php3  9237  suppr  9496  infdif  10234  axdclem2  10545  gchen1  10650  grumap  10833  grudomon  10842  mul32  11412  add32  11464  subsub23  11497  subadd23  11504  addsub12  11505  subsub  11522  subsub3  11524  sub32  11526  suble  11724  lesub  11725  ltsub23  11726  ltsub13  11727  ltleadd  11729  div32  11925  div13  11926  div12  11927  divdiv32  11955  cju  12241  infssuzle  12948  ioo0  13384  ico0  13405  ioc0  13406  icc0  13407  fzen  13553  modcyc  13907  expgt0  14096  expge0  14099  expge1  14100  2cshwcom  14802  shftval2  15058  abs3dif  15314  divalgb  16384  submrc  17611  mrieqv2d  17622  pltnlt  18335  pltn2lp  18336  tosso  18414  latnle  18468  latabs1  18470  lubel  18509  ipopos  18531  grpinvcnv  18971  mulgaddcom  19061  mulgneg2  19071  oppgmnd  19320  oddvdsnn0  19511  oddvds  19514  odmulg  19523  odcl2  19532  lsmcomx  19823  srgcom4  20166  srgrmhm  20174  ringcom  20228  mulgass2  20257  opprrng  20296  irredrmul  20378  irredlmul  20379  isdrngrd  20670  isdrngrdOLD  20672  islmodd  20761  lmodcom  20803  rmodislmod  20825  rmodislmodOLD  20826  opprdomn  21268  zntoslem  21507  ipcl  21582  evls1fpws  22313  maducoevalmin1  22598  rintopn  22855  opnnei  23068  restin  23114  cnpnei  23212  cnprest  23237  ordthaus  23332  kgen2ss  23503  hausflim  23929  fclsfnflim  23975  cnpfcf  23989  opnsubg  24056  cuspcvg  24250  psmetsym  24260  xmetsym  24297  ngpdsr  24558  ngpds2r  24560  ngpds3r  24562  clmmulg  25072  cphipval2  25213  iscau2  25249  dgr1term  26239  cxpeq0  26657  cxpge0  26662  relogbzcl  26751  negsunif  28013  grpoidinvlem2  30387  grpoinvdiv  30419  nvpncan  30536  nvabs  30554  ipval2lem2  30586  dipcj  30596  diporthcom  30598  dipdi  30725  dipassr  30728  dipsubdi  30731  hlipcj  30793  hvadd32  30916  hvsub32  30927  his5  30968  hoadd32  31665  hosubsub  31699  unopf1o  31798  adj2  31816  adjvalval  31819  adjlnop  31968  leopmul2i  32017  cvntr  32174  mdsymlem5  32289  sumdmdii  32297  supxrnemnf  32620  odutos  32784  tlt2  32785  tosglblem  32790  archiabl  32998  unitdivcld  33633  bnj605  34669  bnj607  34678  fisshasheq  34855  swrdrevpfx  34857  cusgredgex  34862  acycgr1v  34890  gcd32  35474  cgrrflx  35714  cgrcom  35717  cgrcomr  35724  btwntriv1  35743  cgr3com  35780  colineartriv2  35795  segleantisym  35842  seglelin  35843  btwnoutside  35852  clsint2  35944  dissneqlem  36950  ftc1anclem5  37301  heibor1  37414  rngoidl  37628  ispridlc  37674  opltcon3b  38806  cmtcomlemN  38850  cmtcomN  38851  cmt3N  38853  cmtbr3N  38856  cvrval2  38876  cvrnbtwn4  38881  leatb  38894  atlrelat1  38923  hlatlej2  38978  hlateq  39002  hlrelat5N  39004  snatpsubN  39353  pmap11  39365  paddcom  39416  sspadd2  39419  paddss12  39422  cdleme51finvN  40159  cdleme51finvtrN  40161  cdlemeiota  40188  cdlemg2jlemOLDN  40196  cdlemg2klem  40198  cdlemg4b1  40212  cdlemg4b2  40213  trljco2  40344  tgrpabl  40354  tendoplcom  40385  cdleml6  40584  erngdvlem3-rN  40601  dia11N  40651  dib11N  40763  dih11  40868  uzindd  41579  lcmineqlem1  41632  nerabdioph  42371  monotoddzzfi  42505  fzneg  42545  jm2.19lem2  42553  ismnushort  43880  nzss  43896  sineq0ALT  44518  lincvalsng  47670  reccot  48375