Theorem 3com23 1126

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 1125	. 2 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
3	2	3com12 1123	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3coml  1127  3anidm13  1421  eqreu  3717  f1ofveu  7407  curry2f  8115  dfsmo2  8369  nneob  8676  nadd32  8717  f1oeng  8993  domnsymfi  9222  sdomdomtrfi  9223  domsdomtrfi  9224  php  9229  php3  9231  fodomfir  9350  suppr  9493  infdif  10230  axdclem2  10542  gchen1  10647  grumap  10830  grudomon  10839  mul32  11409  add32  11462  subsub23  11495  subadd23  11502  addsub12  11503  subsub  11521  subsub3  11523  sub32  11525  suble  11723  lesub  11724  ltsub23  11725  ltsub13  11726  ltleadd  11728  div32  11924  div13  11925  div12  11926  divdiv32  11957  cju  12244  infssuzle  12955  ioo0  13394  ico0  13415  ioc0  13416  icc0  13417  fzen  13563  modcyc  13928  expgt0  14118  expge0  14121  expge1  14122  2cshwcom  14836  shftval2  15096  abs3dif  15352  divalgb  16423  submrc  17642  mrieqv2d  17653  pltnlt  18354  pltn2lp  18355  tosso  18433  latnle  18487  latabs1  18489  lubel  18528  ipopos  18550  grpinvcnv  18993  mulgaddcom  19085  mulgneg2  19095  oppgmnd  19341  oddvdsnn0  19530  oddvds  19533  odmulg  19542  odcl2  19551  lsmcomx  19842  srgcom4  20179  srgrmhm  20187  ringcom  20245  mulgass2  20274  opprrng  20313  irredrmul  20395  irredlmul  20396  isdrngrd  20734  isdrngrdOLD  20736  islmodd  20832  lmodcom  20874  rmodislmod  20896  zntoslem  21529  ipcl  21605  evls1fpws  22321  maducoevalmin1  22606  rintopn  22863  opnnei  23074  restin  23120  cnpnei  23218  cnprest  23243  ordthaus  23338  kgen2ss  23509  hausflim  23935  fclsfnflim  23981  cnpfcf  23995  opnsubg  24062  cuspcvg  24255  psmetsym  24265  xmetsym  24302  ngpdsr  24562  ngpds2r  24564  ngpds3r  24566  clmmulg  25070  cphipval2  25211  iscau2  25247  dgr1term  26235  cxpeq0  26656  cxpge0  26661  relogbzcl  26753  negsunif  28023  grpoidinvlem2  30452  grpoinvdiv  30484  nvpncan  30601  nvabs  30619  ipval2lem2  30651  dipcj  30661  diporthcom  30663  dipdi  30790  dipassr  30793  dipsubdi  30796  hlipcj  30858  hvadd32  30981  hvsub32  30992  his5  31033  hoadd32  31730  hosubsub  31764  unopf1o  31863  adj2  31881  adjvalval  31884  adjlnop  32033  leopmul2i  32082  cvntr  32239  mdsymlem5  32354  sumdmdii  32362  supxrnemnf  32709  odutos  32897  tlt2  32898  tosglblem  32903  archiabl  33144  unitdivcld  33859  bnj605  34880  bnj607  34889  fisshasheq  35079  swrdrevpfx  35081  cusgredgex  35086  acycgr1v  35113  gcd32  35708  cgrrflx  35947  cgrcom  35950  cgrcomr  35957  btwntriv1  35976  cgr3com  36013  colineartriv2  36028  segleantisym  36075  seglelin  36076  btwnoutside  36085  clsint2  36289  dissneqlem  37300  ftc1anclem5  37663  heibor1  37776  rngoidl  37990  ispridlc  38036  opltcon3b  39164  cmtcomlemN  39208  cmtcomN  39209  cmt3N  39211  cmtbr3N  39214  cvrval2  39234  cvrnbtwn4  39239  leatb  39252  atlrelat1  39281  hlatlej2  39336  hlateq  39360  hlrelat5N  39362  snatpsubN  39711  pmap11  39723  paddcom  39774  sspadd2  39777  paddss12  39780  cdleme51finvN  40517  cdleme51finvtrN  40519  cdlemeiota  40546  cdlemg2jlemOLDN  40554  cdlemg2klem  40556  cdlemg4b1  40570  cdlemg4b2  40571  trljco2  40702  tgrpabl  40712  tendoplcom  40743  cdleml6  40942  erngdvlem3-rN  40959  dia11N  41009  dib11N  41121  dih11  41226  uzindd  41937  lcmineqlem1  41989  nerabdioph  42783  monotoddzzfi  42917  fzneg  42957  jm2.19lem2  42965  ismnushort  44277  nzss  44293  sineq0ALT  44914  lincvalsng  48291  reccot  49285