Theorem 3com23 1124

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3coml  1125  3anidm13  1418  eqreu  3659  f1ofveu  7250  curry2f  7919  dfsmo2  8149  nneob  8446  f1oeng  8714  domtrfi  8938  suppr  9160  infdif  9896  axdclem2  10207  gchen1  10312  grumap  10495  grudomon  10504  mul32  11071  add32  11123  subsub23  11156  subadd23  11163  addsub12  11164  subsub  11181  subsub3  11183  sub32  11185  suble  11383  lesub  11384  ltsub23  11385  ltsub13  11386  ltleadd  11388  div32  11583  div13  11584  div12  11585  divdiv32  11613  cju  11899  infssuzle  12600  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  fzen  13202  modcyc  13554  expgt0  13744  expge0  13747  expge1  13748  2cshwcom  14457  shftval2  14714  abs3dif  14971  divalgb  16041  submrc  17254  mrieqv2d  17265  pltnlt  17973  pltn2lp  17974  tosso  18052  latnle  18106  latabs1  18108  lubel  18147  ipopos  18169  grpinvcnv  18558  mulgaddcom  18642  mulgneg2  18652  oppgmnd  18876  oddvdsnn0  19067  oddvds  19070  odmulg  19078  odcl2  19087  lsmcomx  19372  srgrmhm  19687  ringcom  19733  mulgass2  19755  opprring  19788  irredrmul  19864  irredlmul  19865  isdrngrd  19932  islmodd  20044  lmodcom  20084  rmodislmod  20106  rmodislmodOLD  20107  opprdomn  20485  zntoslem  20676  ipcl  20750  maducoevalmin1  21709  rintopn  21966  opnnei  22179  restin  22225  cnpnei  22323  cnprest  22348  ordthaus  22443  kgen2ss  22614  hausflim  23040  fclsfnflim  23086  cnpfcf  23100  opnsubg  23167  cuspcvg  23361  psmetsym  23371  xmetsym  23408  ngpdsr  23667  ngpds2r  23669  ngpds3r  23671  clmmulg  24170  cphipval2  24310  iscau2  24346  dgr1term  25326  cxpeq0  25738  cxpge0  25743  relogbzcl  25829  grpoidinvlem2  28768  grpoinvdiv  28800  nvpncan  28917  nvabs  28935  ipval2lem2  28967  dipcj  28977  diporthcom  28979  dipdi  29106  dipassr  29109  dipsubdi  29112  hlipcj  29174  hvadd32  29297  hvsub32  29308  his5  29349  hoadd32  30046  hosubsub  30080  unopf1o  30179  adj2  30197  adjvalval  30200  adjlnop  30349  leopmul2i  30398  cvntr  30555  mdsymlem5  30670  sumdmdii  30678  supxrnemnf  30993  odutos  31148  tlt2  31149  tosglblem  31154  archiabl  31354  unitdivcld  31753  bnj605  32787  bnj607  32796  fisshasheq  32973  swrdrevpfx  32978  cusgredgex  32983  acycgr1v  33011  gcd32  33621  cgrrflx  34216  cgrcom  34219  cgrcomr  34226  btwntriv1  34245  cgr3com  34282  colineartriv2  34297  segleantisym  34344  seglelin  34345  btwnoutside  34354  clsint2  34445  dissneqlem  35438  ftc1anclem5  35781  heibor1  35895  rngoidl  36109  ispridlc  36155  opltcon3b  37145  cmtcomlemN  37189  cmtcomN  37190  cmt3N  37192  cmtbr3N  37195  cvrval2  37215  cvrnbtwn4  37220  leatb  37233  atlrelat1  37262  hlatlej2  37317  hlateq  37340  hlrelat5N  37342  snatpsubN  37691  pmap11  37703  paddcom  37754  sspadd2  37757  paddss12  37760  cdleme51finvN  38497  cdleme51finvtrN  38499  cdlemeiota  38526  cdlemg2jlemOLDN  38534  cdlemg2klem  38536  cdlemg4b1  38550  cdlemg4b2  38551  trljco2  38682  tgrpabl  38692  tendoplcom  38723  cdleml6  38922  erngdvlem3-rN  38939  dia11N  38989  dib11N  39101  dih11  39206  uzindd  39913  lcmineqlem1  39965  nerabdioph  40547  monotoddzzfi  40680  fzneg  40720  jm2.19lem2  40728  ismnushort  41808  nzss  41824  sineq0ALT  42446  lincvalsng  45645  reccot  46346