Theorem 3com23 1263

Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com23	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1256	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 84	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	3imp 1249	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3coml  1264  syld3an2  1365  3anidm13  1376  eqreu  3365  f1ofveu  6544  curry2f  7160  dfsmo2  7331  nneob  7619  f1oeng  7860  suppr  8260  infdif  8914  axdclem2  9225  gchen1  9326  grumap  9509  grudomon  9518  mul32  10082  add32  10133  subsub23  10165  subadd23  10172  addsub12  10173  subsub  10190  subsub3  10192  sub32  10194  suble  10385  lesub  10386  ltsub23  10387  ltsub13  10388  ltleadd  10390  div32  10584  div13  10585  div12  10586  divdiv32  10612  cju  10893  infssuzle  11647  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  fzen  12229  elfz1b  12279  modcyc  12567  expgt0  12755  expge0  12758  expge1  12759  2cshwcom  13413  shftval2  13663  abs3dif  13919  divalgb  14965  submrc  16111  mrieqv2d  16122  pltnlt  16791  pltn2lp  16792  tosso  16859  latnle  16908  latabs1  16910  lubel  16945  ipopos  16983  grpinvcnv  17306  mulgneg2  17398  oppgmnd  17607  oddvdsnn0  17786  oddvds  17789  odmulg  17796  odcl2  17805  lsmcomx  18082  srgrmhm  18359  ringcom  18402  mulgass2  18424  opprring  18454  irredrmul  18530  irredlmul  18531  isdrngrd  18596  islmodd  18692  lmodcom  18732  opprdomn  19122  zntoslem  19724  ipcl  19797  maducoevalmin1  20277  rintopn  20539  opnnei  20734  restin  20780  cnpnei  20878  cnprest  20903  ordthaus  20998  kgen2ss  21168  hausflim  21595  fclsfnflim  21641  cnpfcf  21655  opnsubg  21721  cuspcvg  21915  psmetsym  21925  xmetsym  21962  ngpdsr  22219  ngpds2r  22221  ngpds3r  22223  clmmulg  22709  cphipval2  22848  iscau2  22883  dgr1term  23820  cxpeq0  24224  cxpge0  24229  relogbzcl  24312  grpoidinvlem2  26743  grpoinvdiv  26775  nvpncan  26893  nvabs  26911  ipval2lem2  26943  dipcj  26953  diporthcom  26955  dipdi  27082  dipassr  27085  dipsubdi  27088  hlipcj  27151  hvadd32  27275  hvsub32  27286  his5  27327  hoadd32  28026  hosubsub  28060  unopf1o  28159  adj2  28177  adjvalval  28180  adjlnop  28329  leopmul2i  28378  cvntr  28535  mdsymlem5  28650  sumdmdii  28658  supxrnemnf  28924  odutos  28994  tlt2  28995  tosglblem  29000  archiabl  29083  unitdivcld  29275  bnj605  30231  bnj607  30240  gcd32  30890  cgrrflx  31264  cgrcom  31267  cgrcomr  31274  btwntriv1  31293  cgr3com  31330  colineartriv2  31345  segleantisym  31392  seglelin  31393  btwnoutside  31402  clsint2  31494  dissneqlem  32363  ftc1anclem5  32659  heibor1  32779  rngoidl  32993  ispridlc  33039  opltcon3b  33509  cmtcomlemN  33553  cmtcomN  33554  cmt3N  33556  cmtbr3N  33559  cvrval2  33579  cvrnbtwn4  33584  leatb  33597  atlrelat1  33626  hlatlej2  33680  hlateq  33703  hlrelat5N  33705  snatpsubN  34054  pmap11  34066  paddcom  34117  sspadd2  34120  paddss12  34123  cdleme51finvN  34862  cdleme51finvtrN  34864  cdlemeiota  34891  cdlemg2jlemOLDN  34899  cdlemg2klem  34901  cdlemg4b1  34915  cdlemg4b2  34916  trljco2  35047  tgrpabl  35057  tendoplcom  35088  cdleml6  35287  erngdvlem3-rN  35304  dia11N  35355  dib11N  35467  dih11  35572  nerabdioph  36391  monotoddzzfi  36525  fzneg  36567  jm2.19lem2  36575  nzss  37538  sineq0ALT  38195  lincvalsng  41999  reccot  42298