Theorem 3com23 1125

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 1124	. 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
3	2	3com12 1122	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3coml  1126  3anidm13  1419  eqreu  3664  f1ofveu  7270  curry2f  7948  dfsmo2  8178  nneob  8486  f1oeng  8759  domnsymfi  8986  sdomdomtrfi  8987  domsdomtrfi  8988  php  8993  php3  8995  suppr  9230  infdif  9965  axdclem2  10276  gchen1  10381  grumap  10564  grudomon  10573  mul32  11141  add32  11193  subsub23  11226  subadd23  11233  addsub12  11234  subsub  11251  subsub3  11253  sub32  11255  suble  11453  lesub  11454  ltsub23  11455  ltsub13  11456  ltleadd  11458  div32  11653  div13  11654  div12  11655  divdiv32  11683  cju  11969  infssuzle  12671  ioo0  13104  ico0  13125  ioc0  13126  icc0  13127  fzen  13273  modcyc  13626  expgt0  13816  expge0  13819  expge1  13820  2cshwcom  14529  shftval2  14786  abs3dif  15043  divalgb  16113  submrc  17337  mrieqv2d  17348  pltnlt  18058  pltn2lp  18059  tosso  18137  latnle  18191  latabs1  18193  lubel  18232  ipopos  18254  grpinvcnv  18643  mulgaddcom  18727  mulgneg2  18737  oppgmnd  18961  oddvdsnn0  19152  oddvds  19155  odmulg  19163  odcl2  19172  lsmcomx  19457  srgrmhm  19772  ringcom  19818  mulgass2  19840  opprring  19873  irredrmul  19949  irredlmul  19950  isdrngrd  20017  islmodd  20129  lmodcom  20169  rmodislmod  20191  rmodislmodOLD  20192  opprdomn  20572  zntoslem  20764  ipcl  20838  maducoevalmin1  21801  rintopn  22058  opnnei  22271  restin  22317  cnpnei  22415  cnprest  22440  ordthaus  22535  kgen2ss  22706  hausflim  23132  fclsfnflim  23178  cnpfcf  23192  opnsubg  23259  cuspcvg  23453  psmetsym  23463  xmetsym  23500  ngpdsr  23761  ngpds2r  23763  ngpds3r  23765  clmmulg  24264  cphipval2  24405  iscau2  24441  dgr1term  25421  cxpeq0  25833  cxpge0  25838  relogbzcl  25924  grpoidinvlem2  28867  grpoinvdiv  28899  nvpncan  29016  nvabs  29034  ipval2lem2  29066  dipcj  29076  diporthcom  29078  dipdi  29205  dipassr  29208  dipsubdi  29211  hlipcj  29273  hvadd32  29396  hvsub32  29407  his5  29448  hoadd32  30145  hosubsub  30179  unopf1o  30278  adj2  30296  adjvalval  30299  adjlnop  30448  leopmul2i  30497  cvntr  30654  mdsymlem5  30769  sumdmdii  30777  supxrnemnf  31091  odutos  31246  tlt2  31247  tosglblem  31252  archiabl  31452  unitdivcld  31851  bnj605  32887  bnj607  32896  fisshasheq  33073  swrdrevpfx  33078  cusgredgex  33083  acycgr1v  33111  gcd32  33715  cgrrflx  34289  cgrcom  34292  cgrcomr  34299  btwntriv1  34318  cgr3com  34355  colineartriv2  34370  segleantisym  34417  seglelin  34418  btwnoutside  34427  clsint2  34518  dissneqlem  35511  ftc1anclem5  35854  heibor1  35968  rngoidl  36182  ispridlc  36228  opltcon3b  37218  cmtcomlemN  37262  cmtcomN  37263  cmt3N  37265  cmtbr3N  37268  cvrval2  37288  cvrnbtwn4  37293  leatb  37306  atlrelat1  37335  hlatlej2  37390  hlateq  37413  hlrelat5N  37415  snatpsubN  37764  pmap11  37776  paddcom  37827  sspadd2  37830  paddss12  37833  cdleme51finvN  38570  cdleme51finvtrN  38572  cdlemeiota  38599  cdlemg2jlemOLDN  38607  cdlemg2klem  38609  cdlemg4b1  38623  cdlemg4b2  38624  trljco2  38755  tgrpabl  38765  tendoplcom  38796  cdleml6  38995  erngdvlem3-rN  39012  dia11N  39062  dib11N  39174  dih11  39279  uzindd  39985  lcmineqlem1  40037  nerabdioph  40631  monotoddzzfi  40764  fzneg  40804  jm2.19lem2  40812  ismnushort  41919  nzss  41935  sineq0ALT  42557  lincvalsng  45757  reccot  46460