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  3676  f1ofveu  7354  curry2f  8051  dfsmo2  8280  nneob  8585  nadd32  8626  f1oeng  8910  domnsymfi  9127  sdomdomtrfi  9128  domsdomtrfi  9129  php  9134  php3  9136  fodomfir  9231  suppr  9378  infdif  10121  axdclem2  10433  gchen1  10539  grumap  10722  grudomon  10731  mul32  11303  add32  11356  subsub23  11389  subadd23  11396  addsub12  11397  subsub  11415  subsub3  11417  sub32  11419  suble  11619  lesub  11620  ltsub23  11621  ltsub13  11622  ltleadd  11624  div32  11820  div13  11821  div12  11822  divdiv32  11854  cju  12146  infssuzle  12872  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  fzen  13486  modcyc  13856  expgt0  14048  expge0  14051  expge1  14052  2cshwcom  14769  shftval2  15028  abs3dif  15285  divalgb  16364  submrc  17585  mrieqv2d  17596  pltnlt  18295  pltn2lp  18296  tosso  18374  latnle  18430  latabs1  18432  lubel  18471  ipopos  18493  grpinvcnv  18973  mulgaddcom  19065  mulgneg2  19075  oppgmnd  19320  oddvdsnn0  19510  oddvds  19513  odmulg  19522  odcl2  19531  lsmcomx  19822  srgcom4  20186  srgrmhm  20194  ringcom  20252  mulgass2  20281  opprrng  20316  irredrmul  20398  irredlmul  20399  isdrngrd  20734  isdrngrdOLD  20736  islmodd  20852  lmodcom  20894  rmodislmod  20916  zntoslem  21546  ipcl  21623  evls1fpws  22344  maducoevalmin1  22627  rintopn  22884  opnnei  23095  restin  23141  cnpnei  23239  cnprest  23264  ordthaus  23359  kgen2ss  23530  hausflim  23956  fclsfnflim  24002  cnpfcf  24016  opnsubg  24083  cuspcvg  24275  psmetsym  24285  xmetsym  24322  ngpdsr  24580  ngpds2r  24582  ngpds3r  24584  clmmulg  25078  cphipval2  25218  iscau2  25254  dgr1term  26235  cxpeq0  26655  cxpge0  26660  relogbzcl  26751  negsunif  28061  oldfib  28383  grpoidinvlem2  30591  grpoinvdiv  30623  nvpncan  30740  nvabs  30758  ipval2lem2  30790  dipcj  30800  diporthcom  30802  dipdi  30929  dipassr  30932  dipsubdi  30935  hlipcj  30997  hvadd32  31120  hvsub32  31131  his5  31172  hoadd32  31869  hosubsub  31903  unopf1o  32002  adj2  32020  adjvalval  32023  adjlnop  32172  leopmul2i  32221  cvntr  32378  mdsymlem5  32493  sumdmdii  32501  supxrnemnf  32856  odutos  33043  tlt2  33044  tosglblem  33049  archiabl  33274  unitdivcld  34061  bnj605  35065  bnj607  35074  rankfilimb  35261  r1filim  35263  fisshasheq  35313  swrdrevpfx  35315  cusgredgex  35320  acycgr1v  35347  gcd32  35947  cgrrflx  36185  cgrcom  36188  cgrcomr  36195  btwntriv1  36214  cgr3com  36251  colineartriv2  36266  segleantisym  36313  seglelin  36314  btwnoutside  36323  clsint2  36527  dissneqlem  37670  ftc1anclem5  38032  heibor1  38145  rngoidl  38359  ispridlc  38405  opltcon3b  39664  cmtcomlemN  39708  cmtcomN  39709  cmt3N  39711  cmtbr3N  39714  cvrval2  39734  cvrnbtwn4  39739  leatb  39752  atlrelat1  39781  hlatlej2  39836  hlateq  39859  hlrelat5N  39861  snatpsubN  40210  pmap11  40222  paddcom  40273  sspadd2  40276  paddss12  40279  cdleme51finvN  41016  cdleme51finvtrN  41018  cdlemeiota  41045  cdlemg2jlemOLDN  41053  cdlemg2klem  41055  cdlemg4b1  41069  cdlemg4b2  41070  trljco2  41201  tgrpabl  41211  tendoplcom  41242  cdleml6  41441  erngdvlem3-rN  41458  dia11N  41508  dib11N  41620  dih11  41725  uzindd  42431  lcmineqlem1  42482  nerabdioph  43255  monotoddzzfi  43388  fzneg  43428  jm2.19lem2  43436  ismnushort  44746  nzss  44762  sineq0ALT  45381  lincvalsng  48904  reccot  50245