Theorem 3com23 1127

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3coml  1128  3anidm13  1423  eqreu  3675  f1ofveu  7361  curry2f  8058  dfsmo2  8287  nneob  8592  nadd32  8633  f1oeng  8917  domnsymfi  9134  sdomdomtrfi  9135  domsdomtrfi  9136  php  9141  php3  9143  fodomfir  9238  suppr  9385  infdif  10130  axdclem2  10442  gchen1  10548  grumap  10731  grudomon  10740  mul32  11312  add32  11365  subsub23  11398  subadd23  11405  addsub12  11406  subsub  11424  subsub3  11426  sub32  11428  suble  11628  lesub  11629  ltsub23  11630  ltsub13  11631  ltleadd  11633  div32  11829  div13  11830  div12  11831  divdiv32  11863  cju  12155  infssuzle  12881  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  fzen  13495  modcyc  13865  expgt0  14057  expge0  14060  expge1  14061  2cshwcom  14778  shftval2  15037  abs3dif  15294  divalgb  16373  submrc  17594  mrieqv2d  17605  pltnlt  18304  pltn2lp  18305  tosso  18383  latnle  18439  latabs1  18441  lubel  18480  ipopos  18502  grpinvcnv  18982  mulgaddcom  19074  mulgneg2  19084  oppgmnd  19329  oddvdsnn0  19519  oddvds  19522  odmulg  19531  odcl2  19540  lsmcomx  19831  srgcom4  20195  srgrmhm  20203  ringcom  20261  mulgass2  20290  opprrng  20325  irredrmul  20407  irredlmul  20408  isdrngrd  20743  isdrngrdOLD  20745  islmodd  20861  lmodcom  20903  rmodislmod  20925  zntoslem  21536  ipcl  21613  evls1fpws  22334  maducoevalmin1  22617  rintopn  22874  opnnei  23085  restin  23131  cnpnei  23229  cnprest  23254  ordthaus  23349  kgen2ss  23520  hausflim  23946  fclsfnflim  23992  cnpfcf  24006  opnsubg  24073  cuspcvg  24265  psmetsym  24275  xmetsym  24312  ngpdsr  24570  ngpds2r  24572  ngpds3r  24574  clmmulg  25068  cphipval2  25208  iscau2  25244  dgr1term  26225  cxpeq0  26642  cxpge0  26647  relogbzcl  26738  negsunif  28047  oldfib  28369  grpoidinvlem2  30576  grpoinvdiv  30608  nvpncan  30725  nvabs  30743  ipval2lem2  30775  dipcj  30785  diporthcom  30787  dipdi  30914  dipassr  30917  dipsubdi  30920  hlipcj  30982  hvadd32  31105  hvsub32  31116  his5  31157  hoadd32  31854  hosubsub  31888  unopf1o  31987  adj2  32005  adjvalval  32008  adjlnop  32157  leopmul2i  32206  cvntr  32363  mdsymlem5  32478  sumdmdii  32486  supxrnemnf  32841  odutos  33028  tlt2  33029  tosglblem  33034  archiabl  33259  unitdivcld  34045  bnj605  35049  bnj607  35058  rankfilimb  35245  r1filim  35247  fisshasheq  35297  swrdrevpfx  35299  cusgredgex  35304  acycgr1v  35331  gcd32  35931  cgrrflx  36169  cgrcom  36172  cgrcomr  36179  btwntriv1  36198  cgr3com  36235  colineartriv2  36250  segleantisym  36297  seglelin  36298  btwnoutside  36307  clsint2  36511  dissneqlem  37656  ftc1anclem5  38018  heibor1  38131  rngoidl  38345  ispridlc  38391  opltcon3b  39650  cmtcomlemN  39694  cmtcomN  39695  cmt3N  39697  cmtbr3N  39700  cvrval2  39720  cvrnbtwn4  39725  leatb  39738  atlrelat1  39767  hlatlej2  39822  hlateq  39845  hlrelat5N  39847  snatpsubN  40196  pmap11  40208  paddcom  40259  sspadd2  40262  paddss12  40265  cdleme51finvN  41002  cdleme51finvtrN  41004  cdlemeiota  41031  cdlemg2jlemOLDN  41039  cdlemg2klem  41041  cdlemg4b1  41055  cdlemg4b2  41056  trljco2  41187  tgrpabl  41197  tendoplcom  41228  cdleml6  41427  erngdvlem3-rN  41444  dia11N  41494  dib11N  41606  dih11  41711  uzindd  42417  lcmineqlem1  42468  nerabdioph  43237  monotoddzzfi  43370  fzneg  43410  jm2.19lem2  43418  ismnushort  44728  nzss  44744  sineq0ALT  45363  lincvalsng  48892  reccot  50233